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)
- Streams.v (File of the standard library).
- EqD.v (some preliminaries about "eq_dep"
of the standard library).
- sampled_streams.v
(definition + properties of "sampled streams").
- lucid_ops.v (data-flow operators of
Lucid-Synchrone).
- sp_rec.v (Recursive constructions).
- examples.v (examples of research
report and some more).
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.
TODO
- 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