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

Displayed time zone: Tijuana, Baja California change

15:50 - 16:40
Dependent TypesResearch Papers at Watercourt
Chair(s): Karl Crary Carnegie Mellon University
15:50
25m
Talk
Up-to Techniques Using Sized Types
Research Papers
Nils Anders Danielsson University of Gothenburg, Chalmers University of Technology
16:15
25m
Talk
Decidability of Conversion for Type Theory in Type Theory
Research Papers
Andreas Abel Gothenburg University, Joakim Öhman IMDEA Software Institute, Andrea Vezzosi Chalmers University of Technology