Journal article

Cogent: Uniqueness types and certifying compilation

L O'Connor, Z Chen, C Rizkallah, V Jackson, S Amani, G Klein, T Murray, T Sewell, G Keller

Journal of Functional Programming | Cambridge University Press (CUP) | Published : 2021


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 verificat..

View full abstract