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

https://hal.inria.fr/hal-03287572
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

File

jfla.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

  • HAL Id : hal-03287572, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

49

Files downloads

71