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 Apr 21 2020 16.00 - 17.00 LFCS seminar: 21 April 2020 - Peter Lumsdaine Speaker: Peter Lumsdaine Blackboard Collaborate: https://eu.bbcollab.com/guest/c9da9829ca3d43a0a597515e8ea0258c
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 Apr 21 2020 16.00 - 17.00 LFCS seminar: 21 April 2020 - Peter Lumsdaine Speaker: Peter Lumsdaine Blackboard Collaborate: https://eu.bbcollab.com/guest/c9da9829ca3d43a0a597515e8ea0258c
