Paper Info
Title
COGENT: Certified Compilation for a Functional Systems Language.
Abstract
We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing such as file systems or network protocol control code. For a well-typed COGENT program, the compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly implements this embedding. The aim is for proof engineers to reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. We describe the formal verification stages of the compiler, which include automated formal refinement calculi, a switch from imperative update semantics to functional value semantics formally justified by the linear type system, and a number of standard compiler phases such as type checking and monomorphisation. The compiler certificate is a series of language-level meta proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.
Year
Venue
Field
2016
arXiv: Programming Languages
HOL,Object code,Programming language,Functional compiler,Computer science,Compiler correctness,Theoretical computer science,Code generation,Compiler,Compiler construction,Formal verification
DocType
Volume
Citations 
Journal
abs/1601.05520
1
PageRank 
References 
Authors
0.36
4
11
Name
Order
Citations
PageRank
Liam O'Connor1445.02
Christine Rizkallah27514.05
Zilin Chen3232.53
Sidney Amani4675.00
Japheth Lim5402.95
Yutaka Nagashima6236.13
Thomas Sewell791437.60
Alex Hixon810.36
Gabriele Keller965736.02
Toby Murray1024217.03
Gerwin Klein11145087.47