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
POPL-2018-papers15:50 - 16:15
Nils Anders DanielssonUniversity of Gothenburg, Chalmers University of Technology
POPL-2018-papers16:15 - 16:40
Andreas AbelGothenburg University, Joakim ÖhmanIMDEA Software Institute, Andrea VezzosiChalmers University of Technology