Towards an efficient and formally-verified convertibility checker

Nathanaëlle Courant’s Ph.D. defense

I defended my Ph.D. on Thursday, September 19th at 2pm, at Inria Paris: 48 rue Barrault, 75013 Paris; in Amphithéâtre Jacques-Louis Lions. A copy of the manuscript can be found here, and a link to the Coq development can be found here. The slides for the defense are also available here.

Abstract

The convertibility test, which checks if two λ-terms are equal up to β-reduction, is an essential part of typechecking and proof verification in proofs assistants based on type theory, such as Coq, Agda and Lean. Naturally, the correctness of such a test is necessary to ensure the proofs thus verified are valid; but having an efficient test is also required both for real-time interaction with the user, and for proof search. In this thesis, we start by proposing an efficient, strong call-by-need, big-step semantics for the λ-calculus, which is the critical building block to implement a convertibility test in a classical manner. This semantics is almost mechanically derived from the semantics of small-step leftmost-outermost reduction of the λ-calculus, by converting them to big-step semantics, adding environments to avoid substitution, and memoizing evaluations. So-called transfer lemmas enable the sharing of computations that are not obviously identical. We then show how we can improve upon this by considering the convertibility problem in its entirety, viewing it as proof search. To this end, we study what can be considered a (non-)convertibility proof, drawing upon existing work. This gives rise to a new parallel, heuristic-less algorithm for this test, which does not duplicate computations, and comes with worst-case complexity guarantees. We derived a virtual machine from this algorithm, and made it more efficient by following Grégoire and Leroy, showing that our algorithm is suited to compilation of the input λ-terms for additional efficiency. Both this semantics and this efficient parallel convertibility test have been implemented in OCaml and experimentally validated, significantly outperforming Coq in some cases. They are also both formalised and verified using Coq, building confidence in our work.