Decidability of Conversion for Type Theory in Type Theory by Andreas Abel, Joakim Öhman, Andrea Vezzosi, POPL 2018 #16
Description
Decidability of Conversion for Type Theory in Type Theory by Andreas Abel, Joakim Öhman, Andrea Vezzosi, POPL 2018
Abstract
Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other words, to check whether two types are convertible. We have formalized in Agda a practical conversion checking algorithm for a dependent type theory with one universe à la Russell, natural numbers, and η-equality for Π types. We prove the algorithm correct via a Kripke logical relation parameterized by a suitable notion of equivalence of terms. We then instantiate the parameterized fundamental lemma twice: once to obtain canonicity and injectivity of type formers, and once again to prove the completeness of the algorithm. Our proof relies on inductive-recursive definitions, but not on the uniqueness of identity proofs. Thus, it is valid in variants of intensional Martin-Löf Type Theory as long as they support induction-recursion, for instance, Extensional, Observational, or Homotopy Type Theory.
Why are you interested in it or why should it be a good idea?
This paper is one of the first formalizations of metatheory of dependent type theory in a proof assistant. Since I worked on extending the formalization, I would like to present it. I expect the presentation will introduce logical relations, which is a standard proof technique in PL research and then point out some of the complications of doing it in a proof assistant and doing it for dependent type theory.
Related work
- Similar proof for STLC - Perhaps it is a good idea to start with this
- the most recent paper about the formalization
- the current formalization
Notes
- Would probably like to present this during October
- I probably do not have to permisions to assign this to me and to add the types tag