Implementing Dependent Type Theory Inhabitation and Unification
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917305504497664 |
|---|---|
| author | Norman, Chase Avigad, Jeremy |
| author_facet | Norman, Chase Avigad, Jeremy |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_01463 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Implementing Dependent Type Theory Inhabitation and Unification Norman, Chase Avigad, Jeremy Logic in Computer Science I.2.3; F.4.1 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. |
| title | Implementing Dependent Type Theory Inhabitation and Unification |
| topic | Logic in Computer Science I.2.3; F.4.1 |
| url | https://arxiv.org/abs/2603.01463 |