BBB room access code 349356
1 April 2021 - 14h00
[FormalProofs] A formally-verified compiler from Esterel to circuits
by Lionel Rieg from VERIMAG / IIM Grenoble INP
Abstract: Esterel is a synchronous programming language (like Lustre or Signal) which can be compiled down to digital circuits, as described for instance in G. Berry's draft book: The Constructive Semantics of Pure Esterel. The goal of this work is to provide a mechanized proof of the correctness of this compilation scheme.
In this talk, after a brief description of the Esterel high-level semantics, I will describe the chain of semantics linking this high-level semantics to the circuit one. Then, I will focus on the last two: the microstep semantics (based on Scott semantics) on the Esterel source code and its translation into the circuit semantics, with the related Coq challenges.
