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 sections can already by proven using classical methods, even if there should be interesting things to do on this part too.