Towards an efficient and formally-verified convertibility checker

Overview & Synopsis

The convertibility test, which checks if two lambda-terms are equal up to beta-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 lambda-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 lambda-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 lambda-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.