LFCS seminar: 21 April 2020 - Peter Lumsdaine

Title: General definitions of dependent type theories

Abstract:

Since Per Martin-Löf introduced intuitionistic dependent type theory in 1972, many extensions and variations of it have been studied. These various dependent type theories have many differences, but also many commonalities.  So one expects that there should be a general notion of which all these theories, or at least, many of them, are instances.  Results proven using the general framework should then apply off-the-shelf to the various individual theories of interest.

Existing approaches (e.g. logical frameworks) are good in many ways, but not fully satisfactory: they have various mismatches with how individual DTT’s are studied in practice.  Most importantly, they don’t yield the standard categorical semantics in terms of contextual categories (or CwA’s, CwF’s, etc.) with extra structure.

I will discuss recent proposals by several researchers delineating general classes of type theories: by myself (joint with Bauer and Haselwarter); by Brunerie; by Isaev; and by Uemura.

Affiliation:

Stockholm University