Types, Sets and Constructions

Hausdorff 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:

Spring School, addressed to PhD students and postdocs (one week in May)

Three major workshops

  • Types, Homotopy Type theory, and Verification (June 4 - June 8)
  • Proofs and Computation (July 2 - July 6)
  • Constructive Mathematics (August 6 - August 10)

Those planning to participate include:

Peter Aczel, Tosi Arai, Sergei Artemov, Steve Awodey, Ulrich Berger, Thierry Coquand, Martín Escardó, Sy Friedman, Rosalie Iemhoff, Hajime Ishihara, Gerhard Jäger, Peter Koellner, Ulrich Kohlenbach, Bob Lubarsky, Maria Emilia Maietti, Per Martin-Löf, Paul-André Mellies, Sara Negri, Paulo Oliva, Erik Palmgren, Giuseppe Rosolini, Giovanni Sambin, Dana Scott, Andreas Weiermann, Vladimir Voevodsky, Ihsen Yengui

Online application will open soon.