Skip to Main content Skip to Navigation
Conference papers

Arguments cadencés dans un compilateur Lustre vérifié

Abstract : Lustre is a synchronous language for programming systems as block diagrams from which low-level imperative code is generated automatically. Recent work applies the Coq interactive proof assistant to specify a compiler from a core subset of Lustre to the Clight input language of CompCert from which assembly code is generated. The overall correctness proof connects the stream semantics of Lustre to the imperative semantics of the assembly code. Every stream in a Lustre program is associated with a static ‘clock’ that represents when it is active. Compilation transforms the clocks into conditional statements that control when the corresponding value are calculated. Previous work made the simplifying assumption that the inputs and outputs of any given block shared the same static clock. This paper describes one way to lift this restriction. It requires enriching the static typing rules for clocks and the semantic model, and, to satisfy the Clight semantics, adding a compilation pass to ensure that any variable passed to a function call has been initialized.
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Timothy Bourke Connect in order to contact the contributor
Submitted on : Monday, February 4, 2019 - 11:13:14 AM
Last modification on : Wednesday, June 8, 2022 - 12:50:04 PM
Long-term archiving on: : Sunday, May 5, 2019 - 1:45:08 PM


Files produced by the author(s)


  • HAL Id : hal-02005639, version 1


Timothy Bourke, Marc Pouzet. Arguments cadencés dans un compilateur Lustre vérifié. JFLA 2019 - Les Trentièmes Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. pp.16. ⟨hal-02005639⟩



Record views


Files downloads