Specifications

We aim to use the dependent types and the proof checker of Coq to show some properties on the impure part of concurrent programs. Pure parts can already by proven using classical methods, even if there should be interesting things to do there too.

Free theorems

We know the programs are well-typed because the type system of Coq is supposed sound and because there are no unsafe operators (like Obj.magic).