26th International Symposium on
Logic-Based Program Synthesis and Transformation
LOPSTR 2016

Edinburgh, Scotland UK
September 6-8, 2016

Co-located with PPDP 2016 and SAS 2016

LOPSTR 2016 Invited Talk

Challenges in Compiling Coq

Greg Morrisett, Cornell University, USA (jointly with PPDP)


Abstract. The Coq proof assistant is increasingly used for constructing verified software, including everything from verified micro-kernels to verified databases. Programmers typically write code in Gallina (the core functional language of Coq) and construct proofs about those Gallina programs. Then, through a process of "extraction", the Gallina code is translated to either OCaml, Haskell, or Scheme and compiled by a conventional compiler to produce machine code. Unfortunately, this translation often results in inefficient code, and it fails to take advantage of the dependent types and proofs. Furthermore, it's a bit embarrassing that the process is not formally verified.

Working with Andrew Appel's group at Princeton, we are trying to formalize as much of the process of extraction and compilation as we can, all within Coq. I will talk about both the opportunities this presents, as well as some of the key challenges, including the inability to preserve types through compilation, and the difficulty that axioms present.