Launch of the website

🐓 July 21, 2015 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 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:

  • a type C.I.t for infinite (co-inductive) computations;
  • a type Trace.t for whose who want to separate the specifications from the proofs of use cases;
  • a Lwt.E effect to add arbitrary Lwt commands.
blog comments powered by Disqus