Verified Compilation of the Modular Reset, Finally

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.

Date
Nov 28, 2019 9:45 AM
Location
CAES CNRS - Centre Paul-Langevin
24, rue du Coin
73500 Aussois
Avatar
Lélio Brun
PhD candidate in Computer Science

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