July 21, 2015
Coq.io is a library for writing and proving concurrent applications with inputs–outputs in Coq. In order to centralize the informations about it, I have setup a website on http://coq.io/. I have been lucky to get this domain name, since this gives a direct reference to the IO monad of Haskell, which popularized the idea of clean imperative programming in a functional language.
There is a Getting started page with some basic examples and an introduction to the technique of formal specification by use cases, and links to some reference documentation. The library is still evolving, with three upcoming improvements:
C.I.tfor infinite (co-inductive) computations;
Trace.tfor whose who want to separate the specifications from the proofs of use cases;
Lwt.Eeffect to add arbitrary Lwt commands.