可信编译器L2C的核心翻译步骤及其设计与实现

同步数据流语言（如Lustre）近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好“误编译”问题，近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证，取得了很大的成功，如CompCert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言，以Clight（CompCert中的C语言子集）为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验