Lucid-Synchrone in Coq

This is a joint work between Sylvain Boulmé, Grégoire Hamon and Marc Pouzet of LIP6. Read research report A clocked denotational semantic for Lucid-Synchrone in Coq (S. Boulmé & G. Hamon) for explanations on this experiment.

For more informations on Coq see the Coq page.

News: An article describing this experiment, Certifying synchrony for free , as been accepted, and will be presented at LPAR 2001. The final version of this paper will be available here soon.

COQ FILES (version 6.3.1)

You may download these files and compile them with Coq 6.3.1. They only rely on standard library files (see Makefile). The code given here may change a lot in the future.


Back to the Lucid Synchrone home page