LFCS Seminar: Tuesday, 11 April - Thorsten Altenkirch


Title:          How to define type theories?



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.

Apr 11 2023 -

LFCS Seminar: Tuesday, 11 April - Thorsten Altenkirch

Thorsten Altenkirch, University of Nottingham https://www.cs.nott.ac.uk/~psztxa/

Venue: IF G.03 - this seminar is hybrid.
To attend remotely:
URL: https://ed-ac-uk.zoom.us/j/88068691738
Password: 9M3snTsg