[ICFP'26] Confluence Techniques for Dependent Type Theory with Typed Conversion

Confluence Techniques for Dependent Type Theory with Typed Conversion (Video, ICFP 2026) Thiago Felicissimo, Théo Winterhalter (Inria Rennes, France; Inria, France / LMF, France) Abstract: In the meta-theoretic study of dependent type theory, confluence techniques are powerful tools for establishing the properties required when proving correctness of implementations. Unfortunately, such techniques have historically mostly been studied for type theories with untyped conversion, which are harder to relate to semantics. In this work, we show how to scale confluence techniques to rich dependent type theories with typed conversion. To do this, we prove a confluence theorem for a theory featuring not only function types (without eta) and universes, but also some inductive types (Nat and sums), dependent pairs (without eta), definitional proof irrelevance and a lift type (with eta), allowing to simulate a weak form of explicit cumulativity (as done in Agda). We then show how to extend our framework with a definitionally proof-irrelevant equality in two ways, either with an observational equality or with an eliminator with a non-linear computation rule (as done in Lean), illustrating the extensibility of our approach. With confluence in hand, we then fulfill our promise of showing (partial) correctness of type- and conversion-checking algorithms. Moreover, while our specification for the type theory is fully annotated, which eases the connection with semantics, we prove correctness of algorithms that operate on usual non-annotated terms, an important optimization for real-life implementations. Finally, our results have been fully formalized in Rocq and can serve as a basis for future type theory formalizations. Article: https://doi.org/10.1145/3828691 Supplementary archive: https://doi.org/10.5281/zenodo.20488664 (Badges: Artifacts Available, Artifacts Evaluated — Reusable) ORCID: https://orcid.org/0009-0000-1074-9275, https://orcid.org/0000-0002-9881-3696 Video Tags: Dependent Type Theory, Confluence, Proof Assistants, doi:10.1145/3828691, doi:10.5281/zenodo.20488664, orcid:0009-0000-1074-9275, orcid:0000-0002-9881-3696, Artifacts Available, Artifacts Evaluated — Reusable Presentation at the ICFP 2026 conference, August 25-27, 2026, https://icfp26.sigplan.org/ Sponsored by ACM SIGPLAN.