COGENT：函数系统语言的认证编译
COGENT: Certified Compilation for a Functional Systems Language
摘要：
我们提出了一个自证明编译器的COGENT系统语言。COGENT是一种受限制的、多态的、高阶的、纯函数式的语言，具有线性类型，不需要可信的运行时或垃圾收集器。它编译成高效的C代码，旨在与现有的C函数互操作。该语言适用于具有最小共享的分层系统代码，例如文件系统或网络协议控制代码。对于类型良好的COGENT程序，编译器生成C代码，在Isabelle/HOL中对其语义进行高级浅嵌入，并证明C代码正确实现了此嵌入。其目的是让证明工程师能够高效地、均衡地推理真实世界系统代码的全部语义，同时保持C语言的互操作性和简洁性。我们描述了编译器的形式化验证阶段，其中包括自动化的形式化细化演算，从命令式更新语义到函数值语义的切换，以及一些标准的编译器阶段，如类型检查和单态化。编译器证书是一系列语言级的Meta证明和每个程序的翻译验证阶段，在Isabelle/HOL中组合成一个连贯的顶级定理。
英文摘要：
We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing such as file systems or network protocol control code. For a well-typed COGENT program, the compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly implements this embedding. The aim is for proof engineers to reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. We describe the formal verification stages of the compiler, which include automated formal refinement calculi, a switch from imperative update semantics to functional value semantics formally justified by the linear type system, and a number of standard compiler phases such as type checking and monomorphisation. The compiler certificate is a series of language-level meta proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
