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}
}