Carl Friedrich von Weizsäcker-Zentrum

Celebrating 90 Years of Gödel's Incompleteness Theorems

Topics

The topics of the conference comprise all areas of logic relating in a narrower or wider sense to Gödel's incompleteness results. This includes the history of logic, proof theory, philosophy of mathematics, aspects of incompleteness in computer science and others.

The conference is organised as a collection of workshops for these specific topics.

In memoriam

On April 26, 2021 Thomas Strahm, a dear friend and close colleague of the organizers and many participants of this meeting, passed away at the age of 57 after prolonged health problems. His research was in the best tradition of Gödel's work and we will remember him at this meeting. You find an obituary at the University of Bern.

Important dates

The conference is planned as a hybrid event, taking place online and on site in Tübingen during the week from 5 to 9 July 2021.


Timetable

(provisorial)

  • 5.7. Monday afternoon: Opening. Higher proof theory after Gödel
  • 6.7. Tuesday morning: Computation in face of incompleteness
  • 6.7. Tuesday afternoon: Type theory in type theory
  • 7.7. Wednesday morning:  Cut-elimination and Herbrand's Theorem
  • 7.7. Wednesday afternoon: Provability predicates
  • 8.7. Thursday morning: Diagonalization
  • 8.7. Thursday afternoon: Recursion-theoretic approaches to computation and complexity
  • 9.7. Friday morning: Philosophy of mathematics after Gödel
  • 9.7. Friday afternoon: Aspects of Gödel's unpublished work; Closing Lecture by Jan von Plato

Workshops:

Aspects of Gödel's unpublished work 

Organisers: Maria Hämeen-Ant­tila (University of Helsinki) and Jan von Plato (University of Helsinki)

Invited speakers:

Miloš Adžić (University of Belgrade): Gödel’s Introduction to Deduction: Logic Lectures at Notre Dame

Gödel’s Introduction to Deduction: Logic Lectures at Notre Dame

Miloš Adžić (University of Belgrade):

Gödel taught a one-semester course in basic logic at the University of Notre Dame in the spring of 1939. Among his unpublished writings in the Princeton University Library one can find notebooks with the manuscript of his notes for that course. Together with Kosta Došen, we have prepared an edition of the notes of which we will offer a brief summary and address some of their importance. We will also comment upon parts of Gödel’s manuscript unavailable to us previously, which were only recently brought to our attention by Jan von Plato.  

Maria Hämeen-Ant­tila (University of Helsinki): Gödel’s functional interpretation in context

Gödel’s functional interpretation in context

Maria Hämeen-Ant­tila (University of Helsinki):

Gödel’s functional interpretation of intuitionistic arithmetic was first introduced in a 1958 article published in the journal Dialectica under the title “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”. However, the interpretation itself was first discovered by Gödel in 1941, when he was preparing a lecture course on intuitionistic logic at Princeton.

The main sources for the interpretation that Gödel calls ∑ are the Princeton lecture notes, another lecture (“In what sense is intuitionistic logic constructive?”) given in Yale in April 1941, as well as shorthand notes in the notebook series Arbeitshefte and, to a lesser extent, Resultate Grundlagen. In my presentation, I will discuss the historical development of the functional interpretation based on the lecture notes and the shorthand notebooks. The aim is to give a general idea of what there is to be found in the fragmentary notes contained in the Arbeitshefte series, and how they might be used to better understand the early functional interpretation and the problems Gödel encountered while working on it.

Akihiro Kanamori (Boston University): The Set Theory in Gödel’s Resultate Grundlagen

The Set Theory in Gödel’s Resultate Grundlagen

Akihiro Kanamori (Boston University):

Most of the four notebooks of Gödel’s 1940-1942 Resultate Grundlagen have to do with set theory, and we find here incisive work of remark- able breadth and depth, much of it replicating the best results achieved at the time or anticipating major avenues of research later. Especially conspicuous are his constructions of an Aronszajn tree and a paradoxical decomposition of the sphere, his formulation of relative constructibility and pointwise definability leading to minimal models, his results in Ramsey-type infinite combinatorics, and his exploration of scales of orders of growth in connection with the Contin- uum Hypothesis. On this last, we now see that his intriguing 1970 remarks on the continuum problem had definite anticipations here.

Tim Lethen (Saarland University): Gödel's theological notes

Gödel's theological notes

Tim Lethen (Saarland University):

In the winter semester of 1937/38, Gödel attended about 30 theological lectures, taking notes which are preserved in his Nachlass in Princeton. These notes are supplemented by an extensive list of theological literature as well as by two lists of literally hundreds of remarks and questions concerning the Catholic Church, the Bible, dogmatics, and theology in general.
The talk will present passages from these sources and attempt to shed light on two of Gödel's main theological concerns. The first one focuses on the idea of formalising theology by capturing a few basic terms and concepts, which are then fixed by a set of axioms and developed into a theory by appropriate rules of inference. In a second approach, Catholic dogmas take on the role of axioms, thus allowing – for example – for a logical investigation of differences between the Western and Eastern Church.
Finally, the talk will present material – recently discovered in Gödel's Nachlass – which reveals his remarkably intensive biblical studies.


Computation in face of incompleteness

Organisers: Roberta Bonacina (University of Tübingen) and Peter Schuster (University Verona)

Invited speakers:

Ulrich Berger (Swansea University): TBA

Ulrich Berger (Swansea University):

TBA

Thierry Coquand (University of Gothenburg): TBA

Thierry Coquand (University of Gothenburg): 

TBA

Ulrich Kohlenbach (TU Darmstadt): TBA

Ulrich Kohlenbach (TU Darmstadt):

TBA

Stefan Neuwirth (Université de Franche-Comté): TBA

Stefan Neuwirth (Université de Franche-Comté):

TBA

Daniel Wessel (LMU Munich): TBA

Daniel Wessel (LMU Munich):

TBA


Cut-elimination and Herbrand's Theorem

Organisers: Matthias Baaz (TU Wien) and Anela Lolic (TU Wien)

Invited speakers:

Anela Lolic (TU Wien): TBA

Anela Lolic (TU Wien)

Jan Bydzovsky (TU Wien): TBA

Jan Bydzovsky (TU Wien)

Yong Cheng (Wuhan University): The landscape of Gödel's incompleteness theorems

The landscape of Gödel's incompleteness theorems

Yong Cheng (Wuhan University)

In the first part of the talk, we will give a brief overview of recent 
research on Gödel's incompleteness theorems from the following aspects: (1) 
the  influence of Gödel's incompleteness theorems on foundations of 
mathematics, philosophy and mathematics; (2) different proofs of Gödel's 
incompleteness theorems; (3) generalizations of Gödel's incompleteness 
theorems; (4) the limit of the applicability of the first incompleteness 
theorem (G1); (5) the intensionality problem of Gödel's  second incompleteness 
theorem (G2).

In the second part of the talk, we will focus on our recent work of finding 
the limit of the first incompleteness theorem (G1) w.r.t. interpretation. We 
examine the interpretation degree structure of weak r.e. theories  for which 
G1 hold, and especially on the question whether there is a minimal r.e. theory 
for which G1 holds. We find that the answers depend on the signature of 
language  and the class of theories we consider.

References:
Yong Cheng, Incompleteness for Higher-Order Arithmetic: An Example Based on 
Harrington's Principle, Springer series: Springerbrief in Mathematics, 
Springer, 2019.

Yong Cheng, Finding the limit of incompleteness I.
Bulletin of Symbolic Logic,  Volume 26, Issue 3-4, December 2020, pp. 268-286.

Yong Cheng, Current research on Gödel's incompleteness theorem, online in The 
Bulletin of Symbolic Logic, DOI: 10.1017/bsl.2020.44, 2021.

Lorenzo Sauras (TU Wien): TBA

Lorenzo Sauras (TU Wien): 


Diagonalization

Organisers: Reinhard Kahle (University of Tübingen) and Paulo Santos (FCT NOVA, University of Tübingen)

Invited speakers:

Helen Preiß (Technical University of Darmstadt): TBA

Helen Preiß (Technical University of Darmstadt):

TBA

Saeed Salehi (University of Tabriz): The Diagonalization Lemma — Demystified Hopefully

The Diagonalization Lemma — Demystified Hopefully

Saeed Salehi (University of Tabriz):

The diagonal lemma says that when a computable and injective Gödel coding # is available from the formulas to the closed terms of a fixed language, then for every formula F(x), with x as the only free variable, there exists a sentence S such that ↔ F(#S) holds. Holding may mean that the above equivalence is true in the standard model of natural numbers (the semantic diagonal lemma) or may mean that the equivalence is provable in a sufficiently strong theory such as Robinson's Arithmetic (the syntactic diagonal lemma).

The so-called lemma, first proved by Gödel (1931) for a particular formula F(x), that of unprovability, and explicated by Carnap (1934) for every formula F, has a (couple of) very short but extremely tricky and easy-to-forget proof(s). The (classical) proof is mysterious and a kind
of magical (pulling a rabbit out of a hat), which adds to the confusion on and about the lemma. It can be even said that once this lemma has been mastered and grasped, then the proofs of the theorems of Gödel's first incompleteness, Tarski's undefinability of truth, and Rosser's (strengthening of Gödel's) incompleteness can be easily understood.

In this talk we will give some alternative proofs for the semantic form of this lemma and for its weak syntactic forms. We will see that the lemma is actually equivalent, in a sense, to the above mentioned theorems of Gödel, Tarski, and Rosser. These new results, we hope, will help us in demystifying this wonderful and prolific lemma; though its classic proof may remain in shadow, our new proofs will hopefully shed some light on the true nature of the diagonal lemma.



References

·       SAEED SALEHI, On the Diagonal Lemma of Gödel and Carnap, The
Bulletin of Symbolic Logic
 26:1 (2020) 80—88.

·       SAEED SALEHI, Tarski’s Undefinability Theorem and the Diagonal
Lemma
, Logic Journal of the IGPL (forthcoming).
 

Noson S. Yanofsky (Brooklyn College, CUNY): Diagonalization, Fixed Points, and Self-reference

Diagonalization, Fixed Points, and Self-reference

Noson S. Yanofsky (Brooklyn College, CUNY):

Some of the most profound and famous theorems in mathematics and computer science of the past 150 years can simultaneously be seen as a consequence of diagonalization, as a fixed-point theorem, and as an instance of a self-referential paradox. These results include Cantor's theorems about different levels of infinity; Russell's paradox; Gödel's incompleteness theorem; Turing's halting problem; and much more. Amazingly, all these diverse theorems and all viewpoints can be seen as instances of a single simple theorem of basic category theory. We describe this theorem and show some of the instances. A large part of the talk will be a discussion of diagonalization proofs, fixed point theorems, and self- referential paradoxes that fail to be an instance of this categorical theorem. We will meet another categorical idea that unifies some of these ideas. No category theory is needed for this talk.
 

TBA


Higher proof theory after Gödel

Organisers: Reinhard Kahle (University of Tübingen) and Michael Rathjen (University of Leeds)

Invited speakers:

Anton Freund (Technical University of Darmstadt): A Uniform Picture of Gap Condition and Collapsing Functions

A Uniform Picture of Gap Condition and Collapsing Functions

Anton Freund (Technical University of Darmstadt):

As Gödel showed, in any formal theory for the foundations of mathematics, there are concrete statements that can neither be proved nor
refuted. Mathematical examples of such statements include Kruskal's tree theorem and its strengthening by a gap condition, as shown by H. Friedman. These mathematical independence results are intimately connected to ordinal analysis. The present talk presents a new and very uniform picture of this connection: First, Kruskal's theorem and the Bachmann-Howard ordinal arise by the same construction, applied to partial and linear orders, respectively. Secondly, by iterating this construction, we obtain the gap condition and ordinal collapsing functions. The talk aims to explain the grand lines of this picture in an accessible way. Parts of it are based on joint work with M. Rathjen and A. Weiermann.

Gerhard Jäger (University of Bern): Remembering Thomas Strahm

Remembering Thomas Strahm

Gerhard Jäger (University of Bern):

A brief overview of Thomas Strahm’s scientific activities and the impact of his work will be given.

Annika Kanckos (University of Helsinki): Strong Normalization of Gödel's T

Strong Normalization of Gödel's T

Annika Kanckos (University of Helsinki)

Following (Wilken &) Weiermann's proofs of SN of Gödel's T the main problems with SN can be located to the λ-formulation of T and the generality of the recursor reductions in the successor case. These problems typically lead to a non-unique (ordinal) number assignment showing termination. We will, based on an observation of how to implement Howard's permutation lemma, sketch how a unique assignment can be constructed for the full system T.

Wolfram Pohlers (University of Münster): On the performance of axiom systems. Set universes

On the performance of axiom systems.

Set universes

Wolfram Pohlers (University of Münster):

One of the aims of proof theory is to characterize axiom systems by invariants. Due to Gödel’s second incompleteness theorem it is to be expected that such invariants are unlikely to be finite. Pioneering work in this directions had then been done by Gerhard Gentzen who characterized the axiom system for Peano Arithmetic by the transfinite ordinal ε0. Our aim is to investigate in how far proof–theoretic or- dinals can serve as measures for the performance of axiom system with respect to their intended standard models. The key observation is the “No Enhancement Theorem” which states that the proof–theoretic ordinal of an axiom system will not grow, even if we strengthen it by arbitrary sentences of the elementary diagram of its standard model. Thus the Peano axioms and D(ℕ), the elementary diagram of ℕ augmented by the scheme of Mathematical Induction, share the proof–theoretic ordinal ε0 although D(ℕ) should know everything about ℕ which, due to Gödel, cannot be true for the Peano axioms.

This indicates that the proof–theoretic ordinal of an axiom system A can hardly be a measure for the performance of A with respect to its standard model. It turns out that it rather measures the performance of A with respect to “universes above” its intended standard model. So called impredicative axiom systems axiomatize more than just one universe above its standard model and thus induce a spec- trum of proof–theoretic ordinals. In a previous paper (which will appear in the volume Axiomatic Thinking II, Springer 2021) we studied axiom systems in the language of arithmetic and their spectra in “analytical universes”, i.e. universes whose sets are sets of natural numbers. In the present talk we will indicate how to extend these studies to axiom systems for set theory and set theoretical—especially admissible—universes. We obtain a bridge to abstract α–recursion theory in so far, that the spectra of the investigated axiom systems contain exactly the ordinals which are closed under the α–recursive functions whose totality is provable in the axiom system.

Anton Setzer (Swansea University): TBA

Anton Setzer (Swansea University):

TBA


Philosophy of mathematics after Gödel

Organisers: Laura Crosilla (University of Oslo) and Thomas Piecha (University of Tübingen)

Invited speakers:

Øystein Linnebo (University of Oslo): Potentialism and Critical Plural Logic

Potentialism and Critical Plural Logic

Øystein Linnebo (University of Oslo):

Potentialism is the view that certain types of entity are successively generated, in such a way that it is impossible to complete the process of generation. What is the correct logic for reasoning about all entities of some such type? Under some plausible assumptions, classical first-order logic has been shown to remain valid, whereas the traditional logic of plurals needs to be restricted. Here I seek to answer the open question of what is the correct plural logic for reasoning about such domains. The answer takes the form of a critical plural logic. An unexpected benefit of this new logic is that it paves the way for an alternative analysis of potentialism, which is simpler and more user-friendly than the extant modal analysis.

Mirna Džamonja (IRIF, CNRS & Université de Paris): Truth in mathematics

Truth in mathematics

Mirna Džamonja (IRIF, CNRS & Université de Paris)

Hilbert’s programme was the holy grail of logic in the late 19th century and the early 20th century. It sought to find common logical foundation to the whole of mathematics, where all the mathematical truths would be derivable from the system through a commonly accepted notion of a proof, preferably in an algorithmic manner. Gödel’s Incompleteness theorems, along with Turing’s undecidability, have put an end to this dream. Logic has been integrating that reality ever since. Logicians have learned how to deal with incompleteness, although not everybody has the same philosophical position on it. 

In this talk, we shall move focus on the dual of completeness: the soundness. Formally, there is no reason to question the soundness of our proofs. Heuristically, there is an elephant in the room. Our proofs are becoming uncheckable due to their length, level of sophistication and the partition of the mathematical community into small and very specialised groups which can hardly understand the announcements of each other's theorems. The traditional system of refereeing does not seem to be sufficiently prepared, so serious journals take years to publish as the referees take years to verify and the less serious kind of journals proliferate, feeding on the «  publish or perish  » credo driven by financial needs of the universities. 

It is difficult to propose remedies to this situation. Some of the world’s top mathematicians have noticed and have reacted: Voevodsky, Perelman, the Lean community and yours truly in a joint with Koutsoukou-Argyraki and Paulson.

All of these are tries and, in our opinion, due to the difficulty of implementation which is mostly manual, not likely to resolve the situation in real time. It seems that the soundness problems should be attacked differently. We feel that it is logic that should take over at this point. The logic should help us understand the uncertainty that high level mathematics has become.

Carlo Nicolai (King's College London): Inexhaustibility and Implicit Commitment

Inexhaustibility and Implicit Commitment

Carlo Nicolai (King's College London):

Gödel's incompleteness theorems are often taken to indicate that our mathematical commitments are inexhaustible. Soundness assertions for a mathematical theory T cannot be established in T. However, they appear to be implicit in the acceptance of T. This notion of implicit commitment is often associated with highly technical studies but it remains, so far, an elusive notion. For instance, it is often claimed that the acceptance of a mathematical theory implicitly commits one to the acceptance of a Uniform Reflection Principle for it. However, logicians and philosophers agree that a satisfactory conceptual analysis of the transition from a theory to its reflection principle is still lacking. In the talk I will survey recent proposals to analyse and justify the transition from a theory to its soundness assertions and present some new results and observations. The original material will mainly concern two ways of articulating the notion of implicit commitment: a direct axiomatization of (minimal) implicit commitment, and the analysis of implicit commitment via a primitive truth predicate. 

Gabriella Crocco (Aix-Marseille Université) and Paola Cantù (CNRS): The application of mathematics in Gödel and beyond

The application of mathematics in Gödel and beyond

Gabriella Crocco (Aix-Marseille Université) and  Paola Cantù (CNRS):

The question of the applicability of mathematics to the empirical sciences is crucial in Gödel's philosophy and constitutes a key problem in contemporary philosophy of mathematics. In the first part, the paper emphasizes the importance of applicability in Gödel, suggesting a new reading of Gödel's criticism to Carnap in The Logical Syntax of Language and a comparison with some passages from the unpublished philosophical notebooks Max Phil. In the second part, the paper shows that the question was already central in Frege, Helmholtz and Bettazzi and analyzes its legacy with reference to neologicism and structuralism.
 


Provability predicates

Organisers: Reinhard Kahle (University of Tübingen) and Paulo Santos (FCT NOVA, University of Tübingen)

Invited speakers:

Sergei Artemov (Graduate Center, CUNY): TBA

Sergei Artemov (Graduate Center, CUNY):

TBA

Lev Beklemishev (Steklov Mathematical Institute): TBA

Lev Beklemishev (Steklov Mathematical Institute):

TBA

Taishi Kurahashi (Kobe University): TBA

Taishi Kurahashi (Kobe University)

TBA

Albert Visser (Utrecht University): Provability according to Kreisel, Löb, Feferman

Provability according to Kreisel, Löb, Feferman

Albert Visser (Utrecht University):

In this talk, I discuss three sets of conditions for being a provability predicate: the Kreisel Condition, the Löb Conditions, and Feferman’s Framework for Provability. We review the conditions, have a look at some separating examples and, briefly, discuss the role and place of the sets of conditions.
Secondly, we present the result that every consistent RE theory extending Peano Arithmetic has a provability predicate satisfying all three sets of conditions. We show that this predicate is part of an interesting bi-modal logic. We discuss some applications of the result. If there is still time, we have a brief look at its proof.

Paulo Santos (FCT NOVA, University of Tübingen): Yablo's Paradox Revisited

Yablo's Paradox Revisited

Paulo Santos (FCT NOVA, University of Tübingen)

Stephen Yablo proposed a paradox which, according to his evaluation, does not depend on self-reference. In this talk, we render Yablo’s paradox, first, by the use of an order relation, showing that it does not rely on arithmetic. Secondly, we formalise it in Linear Temporal Logic and in Modal Logic. These formalisations uncover the underlying logical structure of Yablo’s paradox.

Paulo Santos (FCT NOVA, University of Tübingen): Numeral Completeness

Numeral Completeness

Paulo Santos (FCT NOVA, University of Tübingen)

We will present a numeral completeness result that holds for weak theories of arithmetic; more precisely, we are going to prove that, starting from a true sentence, one can express the fact that the sentence is true inside the weak theory using numerals. As an immediate consequence, we will obtain a numeral form of provable consistency. The third main result that we will present shows that there is a primitive recursive function (we will see that this function can also be Kalmar elementary) that outputs, for each n, a proof that n is not a proof of a contradiction in a fixed consistent theory. We will relate our result with late versions of Hilbert's Program.


Recursion-theoretic approaches to computation and complexity

Organisers Jean-Yves Marion (Institut universitaire de France) and Isabel Oitavem (University Lisbon)

Invited speakers:

Sam Buss (University of California, San Diego): TBA

Sam Buss (University of California, San Diego):

TBA

Daniel Leivant (Indiana University Bloomington) [TBC]: TBA

Daniel Leivant (Indiana University Bloomington) [TBC]:

TBA

Simona Ronchi della Rocca (University of Turin): Characterising Probabilistic Termination

Characterising Probabilistic Termination

Simona Ronchi della Rocca (University of Turin):

In the probabilistic setting, termination has a double nature. Namely we speak about Almost Sure Termination (AST) in case the probability of divergence is null, and about Positive Almost Sure Termination (PAST) if the time to termination is finite. PAST implies AST but not viceversa. A powerful tool for proving program termination are intersection type assignment systems, which have been successfully applied to various kind of deterministic calculi. Here I will show how they can be tailored in order to be applied to the probabilistic case: a unique type assignment system, where the intersection is non idempotent, gives a complete characterisation of both kinds of termination. More specifically, any type derivation for a given term M supplies both a lower bound to the expected time to termination for M, and a lower bound to M’s probability of termination. The system is designed for a call-by-value lambda-calculus, enriched with a probabilistic choice, but all the results are robust and hold for the call-by-name calculus too. 

Helmut Schwichtenberg (LMU Munich): Linear Two-Sorted Constructive Arithmetic

Linear Two-Sorted Constructive Arithmetic

Helmut Schwichtenberg (LMU Munich)

We consider a term system in the style of Goedel's system T together with a computation model that allows to faithfully represent
polynomial-time algorithms. To this end we follow a tradition initiated by Simmons (1988) and developed by Bellantoni and Cook (1992), where two sorts of variables are admitted, here called output and input variables. The idea is that input variables are the general ones which may be recursed on and used many times, whereas output variables cannot be recursed on and can be used only once. These ideas have been extended to a higher type setting and hence ­– via the Curry-Howardcorrespondence – to a linear two-sorted arithmetical system in the style of Heyting arithmetic in all finite types. Here we further extend this setup with the aim to also include certain nonlinear algorithms (like treesort), given by constants defined by equations involving multiple recursive calls.


Type theory in type theory

Organsiers: Roberta Bonacina (University of Tübingen) and Peter Schuster (University Verona)

Invited speakers:

Thorsten Altenkirch (University of Nottingham): TBA

Thorsten Altenkirch (University of Nottingham):

TBA

Bruno Barras (Laboratoire Spécification et Vérification): TBA

Bruno Barras (Laboratoire Spécification et Vérification):

TBA

Thierry Coquand (University of Gothenburg): TBA

Thierry Coquand (University of Gothenburg):

TBA

Peter Dybjer (University of Gothenburg): A Note on Generalized Algebraic Theories and Categories with Families

A Note on Generalized Algebraic Theories and Categories with Families

Peter Dybjer (University of Gothenburg):

We give a new syntax independent definition of the notion of a finitely presented generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. To this end we define inductively how to build a valid signature Σ for a generalized algebraic theory and the associated category CwF_Σ of cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notions of uniform family of contexts, types, and terms. Furthermore, we show how to syntactically construct initial cwfs with Σ-structures. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of dependent type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual categories with families.


This is joint work with Marc Bezem, Thierry Coquand, and Martin Escardo.

Ambrus Kaposi (Eötvös-Loránd-University): TBA

Ambrus Kaposi (Eötvös-Loránd-University):

TBA

Peter LeFanu Lumsdaine (Stockholm University): TBA

Peter LeFanu Lumsdaine (Stockholm University):

TBA


Participants

TBA

Organization

The conference is organised by:

Program committee

Matthias Baaz, Reinhard Kahle, Thomas Piecha, Jan von Plato