Cogent: uniqueness types and certifying compilation

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

Full description

Saved in:
Bibliographic Details
Published in:Journal of functional programming 2021-01, Vol.31, Article e25
Main Authors: O’CONNOR, LIAM, CHEN, ZILIN, RIZKALLAH, CHRISTINE, JACKSON, VINCENT, AMANI, SIDNEY, KLEIN, GERWIN, MURRAY, TOBY, SEWELL, THOMAS, KELLER, GABRIELE
Format: Article
Language:English
Subjects:
Functional programming
Garbage
Programming languages
Safety
Secure Compilation
Semantics
Source programs
Uniqueness
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0956-7968
1469-7653
DOI:10.1017/S095679682100023X