Types, Sets and Constructions

Trimester Program

May 2 - August 24, 2018

Organizers: Douglas S. Bridges, Michael Rathjen, Peter Schuster, Helmut Schwichtenberg

Type theory, originally conceived as a bulwark against the paradoxes of naive set theory, has languished for a long time in the shadow of axiomatic set theory which became the mainstream foundation of mathematics. The first renaissance of type theory occurred with the advent of computer science and Bishop's development of a practice-oriented constructive mathematics. It was followed by a second quite recent one that not only champions type theory as a central framework for achieving the goal of fully formalized mathematics amenable to verification by computer-based proof assistants, but also finds deep and unexpected connections between type theory and homotopy theory. Constructive set theory and mathematics distinguishes itself from its traditional counterpart, classical set theory and mathematics based on it, by insisting that proofs of existential theorems must afford means for constructing an instance. Constructive reasoning emerges naturally in core areas of mathematics and in the theory of computation. The aim of the Hausdorff Trimester is to create a forum for research on and dissemination of exciting recent developments, which are of central importance to modern foundations of mathematics.

The program will include the following events:

Summer School, addressed to PhD students and postdocs (May 3-9, 2018, without Sunday, 6^th)

Three major workshops

Those planning to participate include:

Peter Aczel, Toshiyasu Arai, Sergei Artemov, Steve Awodey, Andrej Bauer, Ulrich Berger, Thierry Coquand, Martín Escardó, Rosalie Iemhoff, Hajime Ishihara, Gerhard Jäger, Peter Koellner, Ulrich Kohlenbach, Robert Lubarsky, Maria Emilia Maietti, Per Martin-Löf, Paul-André Mellies, Sara Negri, Paulo Oliva, Erik Palmgren, Giuseppe Rosolini, Giovanni Sambin, Monika Seisenberger, Andreas Weiermann, Ihsen Yengui