Seminar details

Room 306 (3rd floor, badged access)
16 December 2019 - 14h00
Verified Compilation of the Lustre Modular Reset
by Lélio Brun from ENS Ulm



Abstract: We present the formalization of the semantics of the modular reset construct of Lustre, and show how to integrate it into Vélus, a Lustre compiler verified in Coq and built on top of CompCert.
In particular, we introduce a new intermediate language in the compilation chain, specifically designed to handle compilation of the modular reset.



Attention: le séminaire sera en 306 et non en 206 !

Contact | Site Map | Site powered by SPIP 3.1.12 + AHUNTSIC [CC License]

info visites 1573408