Confluence Techniques for Dependent Type Theory with Typed Conversion

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.