Verified Compilation of the Modular Reset, Finally


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.

Nov 28, 2019 9:45 AM
CAES CNRS - Centre Paul-Langevin
24, rue du Coin
73500 Aussois
Lélio Brun
Lélio Brun
Postdoctoral research scientist in Computer Science

My research interests include synchronous languages, functional programming and verified compilation.