A formally verified transformation to unify multiple nested clocks for a Lustre-like language

摘要

＜正＞Multiple nested clocks is a major language feature in synchronous data-flow languages such as Lustre [1]. To build a formally verified compiler for such a language, it is a common practice to compile the source program to a C-like program first before compiling it to low-level machine-dependent code using a formally verified backend compiler