Implementing Dependent Type Theory Inhabitation and Unification
Chase Norman, Jeremy Avigad
TL;DR
A novel implementation of dependent type theory and a monadic framework to transform the type checker into a performant solver for inhabitation and unification in dependent type theory are described.
Abstract
Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synthesis. We introduce Canonical-min, a sound and complete solver for inhabitation and unification in dependent type theory, implemented in 185 lines of Lean code. This paper describes a novel implementation of dependent type theory and a monadic framework to transform the type checker into a performant solver. Finally, we introduce DTTBench, a benchmark for type inhabitation in dependent type theory.