Cogent: uniqueness types and certifying compilation. (27th October 2021)

• Record Type: Journal Article
• Authors: O'CONNOR, LIAM; CHEN, ZILIN; RIZKALLAH, CHRISTINE; JACKSON, VINCENT; AMANI, SIDNEY; KLEIN, GERWIN; MURRAY, TOBY; SEWELL, THOMAS; KELLER, GABRIELE
• Is Part Of: Journal of functional programming. Volume 31(2021)
• Publication Date: 2021-10-27
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S095679682100023X
• Languages: English
• ISSNs: 0956-7968

Abstract

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.