search

brando90 / cs522_project

0 stars 0 forks source link

Coq Concurrency #3

Open brando90 opened 5 years ago

brando90 commented 5 years ago

how do we implement concurrency in Coq?

umenthum commented 5 years ago

Relations allow us to implement concurrency I think, but they make proofs more tedious. We'll avoid non-determinism, in fact I think we can have (and might need) proofs of confluence.