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
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
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.
- Streams.v (File of the standard library).
- EqD.v (some preliminaries about "eq_dep"
of the standard library).
(definition + properties of "sampled streams").
- lucid_ops.v (data-flow operators of
- sp_rec.v (Recursive constructions).
- examples.v (examples of research
report and some more).
- change the notion of "length-fail-preserving" for a more general
(cf. research report).
- port this code to version 7.*
- clean the code.
- comment it using "coqweb" (to extract doc. from the sources).
Back to the Lucid Synchrone home page