Proving a Lustre Compiler Part 2


The compilation of block diagram languages like Lustre or Scade often use an intermediary language between the source data-flow code and the target imperative code. We recently implemented and verified a translation function in Coq from a simple intermediary language towards the CompCert-accepted Clight language.

The intermediary language uses an idealized hierarchical memory representation, whereas Clight uses an intricate memory model rather close of the machine. Our proof of correctness must consequently tackle alignment, aliasing and padding. We use separation logic predicates developed in CompCert to solve those issues.

Dec 7, 2016 5:30 PM
Dominikanerkloster Bamberg
Heiliggrabstraße 24
D-696052 Bamberg

The “Part 1” is a talk presented by Timothy Bourke.

Lélio Brun
Lélio Brun
Postdoctoral research scientist in Computer Science

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