COGENT: Certified Compilation for a Functional Systems Language
arXiv: Programming Languages, Volume abs/1601.05520, 2016.
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...More
PPT (Upload PPT)