Papers With

← All papers
First page of Implementing Dependent Type Theory Inhabitation and Unification

Implementing Dependent Type Theory Inhabitation and Unification

Chase Norman, Jeremy Avigad

cs.LO Mar 2, 2026 · v1
tactic-automation tooling benchmark type-theory
Read PDF arXiv abstract Code
TL;DR
Implements Canonical-min, a sound and complete inhabitation/unification solver for dependent type theory, in 185 lines of Lean, exposed as a Lean tactic.
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.
Problem

Inhabitation and unification are undecidable but useful problems in dependent type theory for theorem proving and program synthesis. Existing solvers do not fully exploit the structure of dependent type theory.

Approach

The authors introduce Canonical-min, a sound and complete solver for inhabitation and unification in dependent type theory, implemented in 185 lines of Lean code. A novel representation of lambda expressions decomposes them into bindings, head, and spine. A monadic framework transforms the type checker into a performant solver. They also introduce DTTBench, a benchmark for type inhabitation.

Results

Canonical-min is implemented in 185 lines of Lean and solves both inhabitation and unification problems. DTTBench provides a standard evaluation benchmark for type inhabitation in dependent type theory.