Détails sur le séminaire


Room 306 (3rd floor, badged access)

16 décembre 2019 - 14h00
Verified Compilation of the Lustre Modular Reset
par Lélio Brun de 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 | Plan du site | Site réalisé avec SPIP 4.2.8 + AHUNTSIC [CC License]

info visites 3885894