Cogent: uniqueness types and certifying compilation

Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller

Research output: Contribution to journalArticlepeer-review

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.
Original languageEnglish
Article numbere25
Number of pages66
JournalJournal of Functional Programming
Volume31
DOIs
Publication statusPublished - 27 Oct 2021

Fingerprint

Dive into the research topics of 'Cogent: uniqueness types and certifying compilation'. Together they form a unique fingerprint.

Cite this