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

Type safety

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).

Exceptions

All exceptions are caught since they must be explicitly typed in a monad. We use the simple error-handlers library to handle exceptions.

Termination

Depending on the interface with the OS we have different termination properties. Of course pure terms terminate. In general, except if there are infinitely many messages sent on a channel, impure programs either terminate or block, waiting for a message.