Implementing Dependent Type Theory Inhabitation and Unification
Logic in Computer Science
2026-03-03 v1
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.
Keywords
Cite
@article{arxiv.2603.01463,
title = {Implementing Dependent Type Theory Inhabitation and Unification},
author = {Chase Norman and Jeremy Avigad},
journal= {arXiv preprint arXiv:2603.01463},
year = {2026}
}