一句话：提出函数式语言 Cogent，其唯一性类型系统无需运行时或 GC 即可保证内存安全，并通过双语义与精化定理实现生成 C 代码的认证编译。
本文提出一个旨在显著降低底层操作系统组件函数正确性证明成本的框架。其核心是一种新的函数式语言 Cogent，其唯一性类型系统无需可信运行时或垃圾回收即可保证内存安全。该语言具有两套语义：面向高效 C 代码生成的命令式语义，以及支持等式推理与高层正确性验证的纯函数式语义。连接两者的精化定理使编译器能够通过翻译确认生成证明，认证生成的 C 代码相对于 Cogent 源程序语义的正确性。最后通过两个文件系统实现展示了该框架在实现与验证方面的有效性。
Abstract This paper presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating systems components. The framework is designed around a new functional programming language, Cogent. A central aspect of the language is its uniqueness type system, which eliminates the need for a trusted runtime or garbage collector while still guaranteeing memory safety, a crucial property for safety and security. Moreover, it allows us to assign two semantics to the language: The first semantics is imperative, suitable for efficient C code generation, and the second is purely functional, providing a user-friendly interface for equational reasoning and verification of higher-level correctness properties. The refinement theorem connecting the two semantics allows the compiler to produce a proof via translation validation certifying the correctness of the generated C code with respect to the semantics of the Cogent source program. We have demonstrated the effectiveness of our framework for implementation and for verification through two file system implementations.
@article{paperbot1247,
title = {Cogent: uniqueness types and certifying compilation},
author = {LIAM O’CONNOR and ZILIN CHEN and CHRISTINE RIZKALLAH and VINCENT JACKSON and SIDNEY AMANI and GERWIN KLEIN and TOBY MURRAY and THOMAS SEWELL and GABRIELE KELLER},
journal = {Journal of Functional Programming},
volume = {31},
year = {2021},
doi = {10.1017/s095679682100023x}
}