Thu 11 Jan 2018 16:15 - 16:40 at Watercourt - Dependent Types Chair(s): Karl Crary

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 $\eta$-equality for $\Pi$ 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.

#### Thu 11 Jan

 15:50 - 16:40: Research Papers - Dependent Types at Watercourt Chair(s): Karl CraryCarnegie Mellon University 15:50 - 16:15Talk Up-to Techniques Using Sized TypesNils Anders DanielssonUniversity of Gothenburg, Chalmers University of Technology 16:15 - 16:40Talk Decidability of Conversion for Type Theory in Type TheoryAndreas AbelGothenburg University, Joakim ÖhmanIMDEA Software Institute, Andrea VezzosiChalmers University of Technology