We express reactive programs in Coq using data-flow synchronous operators. Following Lucid-Synchrone approach, synchronous static constraints are here expressed using dependent types. Hence, our analysis of synchrony is here directly performed by Coq typechecker. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Boulmé, S., & Hamon, G. (2001). Certifying synchrony for free. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2250, 495–506. https://doi.org/10.1007/3-540-45653-8_34
Mendeley helps you to discover research relevant for your work.