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.
The “Part 1” is a talk presented by Timothy Bourke.