Doctoral Thesis: Relational compilation for end-to-end verification

Clement Pit-Claudel

ABSTRACT: Purely functional programs verified using interactive theorem provers typically need to be translated to run: either by extracting them to a similar language (like Coq to OCaml) or by proving them equivalent to a deeply embedded implementation (like a C program).  Traditionally, the first approach was automated but produced unverified programs with average performance, and the second approach was manual but produced verified, high-performance programs.

 This thesis shows how to recast program extraction as a proof-search problem to automatically derive correct-by-construction, high-performance code from shallowly embedded functional programs. First, it introduces a unifying framework, *relational compilation*, to capture and extend recent developments in program extraction, with a focus on modularity and sound extensibility.  Then, it presents Rupicola, a relational compiler-construction toolkit designed to extract fast, verified, idiomatic low-level code from annotated functional models.

 The originality of this approach lies in its combination of extensibility, foundational proofs, and performance, backed by an unconventional take on compiler extensions: unlike traditional compilers, Rupicola generates good code not because of clever built-in optimizations, but because it allows users to soundly plug in domain- and sometimes program-specific extensions.  This thesis demonstrates the benefits of this approach through case studies and performance benchmarks that highlight how easy Rupicola makes it to create domain-specific compilers that generate code with performance comparable to that of handwritten C programs.

Details

• Date: Thursday, December 2
• Time: 10:00 am
• Category: Thesis Defense
• Location: 32-D463 (Star Room)

Additional Location Details:

Thesis Supervisor: Prof. Adam Chlipala