November 8th at 18:30, in ILLC Seminar Room F1.15, Science Park 107, Amsterdam
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.