8 November 2019, Cool Logic, Dominik Wehr

With the Principia Mathematica, Whitehead and Russel famously put forward a type theory as a foundation of mathematics. Since then, events such as the discovery of the Curry-Howard correspondence and the introduction of dependent types have drastically changed the face of type theory. Modern type theories thus give rise to attractive foundations of mathematics which are very different from that of the Principia Mathematica.

The talk will begin with a slightly simplified overview of some of the
inner workings of dependent type theories and their intrinsic logic. This will be followed by a more general discussion of the foundations obtained from such type theories.