LFCS Seminar: Tuesday, 11 April - Thorsten Altenkirch

Title:          How to define type theories?

Abstract

In the past we defined type theories, extrinsically by sorting untyped terms. I will explain the intrinsical approach where we never introduce untyped objects. This can be implemented using Quotient Inductive Inductive Types\ (QIITs) and we can establish basic results like normalisation within this approach. The "initiality theorem" becomes a triviality, the syntax of type theory is an initial algebra by definition.

Some interesting questions are: How do we deal with coherence in the context of Homotopy Type Theory? and How do we model Higher Order Abstract Syntax? If time allows I will try to address those.

This talk is based on joint work with Ambrus Kaposi and subject of ongoing work with Phil Wadler.