Skip to Main content Skip to Navigation
Conference papers

Normalisation vérifiée du langage Lustre

Timothy Bourke 1 Paul Jeanmaire 1 Basile Pesin 1 Marc Pouzet 1 
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique - ENS Paris, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : Lustre is a synchronous dataflow language designed for programming embedded systems. In the Vélus project, we use Coq to develop and formalize a compiler that accepts a normalized form of the language and produces imperative code. While this restricted form is suitable for code generated from a user interface based on block diagrams, we wanted to allow programmers to use the complete language. In this article, we present the normalization pass that transforms the complete language into the normalized one. This transformation is divided into three steps so as to simplify the correctness proofs. To show that the semantics is preserved, it is necessary to prove that the three steps preserve certain static and dynamic properties of the language. In particular, the relation between the clock types and the dynamic semantic must be established.
Complete list of metadata
Contributor : Timothy Bourke Connect in order to contact the contributor
Submitted on : Thursday, July 15, 2021 - 5:10:18 PM
Last modification on : Wednesday, June 8, 2022 - 12:50:05 PM
Long-term archiving on: : Saturday, October 16, 2021 - 6:59:20 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License


  • HAL Id : hal-03287572, version 1



Timothy Bourke, Paul Jeanmaire, Basile Pesin, Marc Pouzet. Normalisation vérifiée du langage Lustre. JFLA 2021 - 32ème Journées Francophones des Langages Applicatifs, Yann Régis-Gianas et Chantal Keller, Apr 2021, En ligne, France. pp.117-133. ⟨hal-03287572⟩



Record views


Files downloads