Time Schedule

Abstracts

Participants

Videos (after the event)

CONFERENCE
​
Type Theory, Constructive Mathematics and Geometric Logic
Théorie des types, mathématiques constructives et logique géométrique

1 - 5 May 2023

Scientific Committee
Comité scientifique

Olivia Caramello (University of Insubria)
Hajime Ishihara (Japan Advanced Institute of Science and Technology)
Henri Lombardi (Université de Franche-Comté)
Erick Palmgren (Stockholm University) was a member of the scientific committee. He passed away in November 2019.  We deeply miss him.
Monika Seisenberger (Swansea University)

Organizing Committee
Comité d'organisation

Thierry Coquand (University of Gothenburg)
Sara Negri (University of Genova)
Michael Rathjen (University of Leeds)
Peter Schuster (University of Verona)

PRE-REGISTER - APPLY HERE

IMPORTANT WARNING:  Scam / Phishing / SMiShing ! Note that ill-intentioned people may be trying to contact some of participants by email or phone to get money and personal details, by pretending to be part of the staff of our conference center (CIRM).  CIRM and the organizers will NEVER contact you by phone on this issue and will NEVER ask you to pay for accommodation/ board / possible registration fee in advance. Any due payment will be taken onsite at CIRM during your stay.

Description

The debate between Hilbert and Brouwer, which took place at the beginning of the 20th century, is without doubt one of the most important events in the history of foundations of mathematics. In that debate Brouwer rejected transcendent proof methods and insisted on the exclusive use of intuitionist (or constructive) arguments for a conceptually correct development of mathematics. Hilbert, on the contrary, viewed these transcendental and non-effective proofs as the very essence of mathematical thinking. He introduced proof theory in the hope to justify these transcendent methods by purely effective means. While Gödel’s second incompleteness theorem is generally said to contravene Hilbert’s hopes, it is remarkable that Gödel himself insisted on the fact that his result does not contradict at all Hilbert’s program. In fact, the impact of Gödel’s result on Hilbert’s program was the topic of a discussion between Gödel, Herbrand and Neumann about the fundamental question of the scope of constructive mathematics.
Recent results in different fields of mathematics, such as proof theory, type theory, constructive algebra and categorical logic, shed new light on this question. For instance, proof theory seems to indicate precise limits to intuitionistic type theory, while on the other hand the Univalence Axiomallows for a rather unexpected extension of constructive methods. The goal of this workshop is precisely to bring together experts in these different fields to evaluate the impact of those new results on foundations of mathematics.

Le débat entre Hilbert et Brouwer, qui a eu lieu au début du 20ème siècle, est sans doute un des évènements les plus importants dans l’histoire des fondements des mathématiques. Dans ce débat, Brouwer rejetait les méthodes de preuve transcendantes et insistait sur l’utilisation exclusive d’arguments intuitionistes (ou constructifs) pour un développement conceptuellement correct des mathématiques. Hilbert au contraire voyait dans ces preuves transcendantes et non effectives l’essence même de la pensée mathématique. Il introduit la théorie de la démonstration dans l’espoir de justifier ces méthodes transcendantes par des arguments purement effectifs. Bien que l’on considère généralement que le deuxième théorème d’incomplétude de Gödel porte un coup d’arrêt à ces espoirs Hilbert, on peut remarquer que Gödel lui-même insiste sur le fait que son résultat ne contredit en rien le programme de Hilbert. En fait, la portée de ce résultat a fait l’objet d’un débat passionnant entre Gödel, Herbrand et Neumann ; ce qui est en jeu dans ce débat est la question fondamentale de quelle est l'étendue des mathématiques constructives.
Des résultats récents, venant de domaines différents comme la théorie de la démonstration, la théorie des types, l’algèbre constructive et la logique catégorique, apportent de nouveaux  éléments sur cette question. Par exemple, la théorie de la démonstration semble indiquer des limites précises à la théorie intuitioniste des types, alors que, d’un autre côté, l’axiome d’univalence permet une extension inattendue des méthodes constructives. Le but de ce workshop est précisément de réunir des experts de ces différents domaines pour évaluer l’impact de ces nouveaux résultats sur les fondements des mathématiques.

Speakers to be confirmed

Sergei Artemov (City University of New York)
Andrej Bauer (University of Ljubljana)
Ulrich Berger (Swansea University)
Ingo Blechschmidt (University of Verona)
Laura Crosilla (University of Oslo)
Hannes Diener (University of Canterbury)
Martin Escardó (University of Birmingham)
Anton Freund (Technical University of Darmstadt)
Peter Lumsdaine (Stockholm University)
Dale Miller (Inria Saclay)
Takako Nemoto (Japan Advanced Institute of Science and Technology)
Thomas Powell (Technical University of Darmstadt)
Chuangjie Xu (Ludwig Maximilian University of Munich)
Ihsen Yengui (University of Sfax)

SPONSOR