Scroll down this page for the abstracts, links to the slides can be found in a separate page.

Wednesday 24th | |
---|---|

8:30-9:00 | Registration |

Morning session | Chair: Ana Bove |

9:00-9:15 | Welcome! |

9:15-10:00 | Gérard Huet: Genesis of the Coq system |

10:00-10:30 | Coffee break |

10:30-11:15 | Xavier Leroy: Programming in type theory, or: How Coq became my favorite programming language |

11:15-12:00 | Andrew Pitts: Thierry Coquand and Constructive type theory — a personal perspective |

12:00-13:45 | Lunch Break |

Afternoon session | Chair: Anders Mörtberg |

13:45-14:30 | Stefan Neuwirth: Thierry Coquand and Paul Lorenzen |

14:30-15:15 | Henri Lombardi: Constructive algebra with Thierry Coquand |

15:15-15:45 | Coffee break |

15:45-16:30 | Peter Schuster: Between transfinite and dynamical proof methods |

16:30-17:15 | Martín Escardó: There are more groups in the next universe |

Thursday 25th | |
---|---|

Morning session | Chair: Peter Lumsdaine |

9:00-9:45 | Steve Awodey: Algebraic type theory |

9:45-10:15 | Coffee break |

10:15-11:00 | Olivia Caramello: Relative toposes as a generalization of locales |

11:00-11:45 | Bas Spitters: A comparison of topological toposes |

11:45-13:45 | Lunch Break |

Afternoon session | Chair: Christian Sattler |

13:45:14:30 | Marc Bezem: Solving universe level constraints |

14:30-15:15 | Thorsten Altenkirch: Investigating the Tarpeian rock : Paradoxes in Type Theorys |

15:15-16:00 | Coffee break |

16:00-16:45 | Hugo Herbelin: Computing with Gödel’s completeness theorem: Weak Fan Theorem, Markov’s Principle and Double Negation Shift in action |

Free time | |

18:30-21:30 | Banquet at Wijkanders restaurant |

Friday 26th | |
---|---|

Morning session | Chair: Andreas Abel |

9:00-9:45 | Helmut Schwichtenberg: Verified algorithms via proofs |

9:45-10:15 | Coffee break |

10:15-11:00 | Ulrich Berger: Extracting concurrent programs from proofs |

11:00-11:45 | Stefano Berardi: On the computational content of the axiom of choice. About a paper with T. Coquand and M. Bezem |

11:45-13:45 | Lunch Break |

Afternoon session | Chair: Peter Dybjer |

13:45-14:30 | Assia Mahboubi: Formalising mathematics, in practice |

14:30-15:15 | Cyril Cohen: Unsolvability of the Quintic Formalized in Dependent Type Theory |

15:15-16:00 | Coffee break |

16:00-16:45 | Anders Mörtberg: Formalizing π₄(𝕊³) ≃ ℤ/2ℤ and computing a Brunerie number in Cubical Agda |

## Abstracts:

Thorsten Altenkirch- University of NottinghamInvestigating the Tarpeian rock : Paradoxes in Type TheoryCoquand showed that Russell's paradox can be implemented in a Type Theory with Type : Type and inductive types. This is a very straightforward construction but it is weaker than Girard's paradox which shows that a Type Theory with two impredicative levels (System U) and only Pi-types is inconsistent. Girard's paradox uses the Burali-Forti paradox about the well-order of all well orderings and is technically more complicated. I will discuss the work of Coquand and Hurken in the quest for a comprehensible and simple paradox.

Steve Awodey- Carnegie Mellon UniversityAlgebraic type theoryA type theoretic universe U* —> U bears an algebraic structure resulting from the type-forming operations of unit type, identity type, dependent sum, and dependent product, which may be generalized to form the concept of a "Martin-Löf algebra". A free ML-algebra is then a model of type theory with special properties. The theory of such ML-algebras can be seen as a proof-relevant version of the theory of Zermelo-Fraenkel algebras from the algebraic set theory of Joyal-Moerdijk.

Stefano Berardi- Università di TorinoOn the computational content of the axiom of choice. About a paper with T. Coquand and M. BezemIn 1993 and 1994 T. Coquand works with D. Fridlender on the constructive interpretation of the classical proofs of Higman Lemma: given an infinite sequence of words w_0, w_1, w_2, ... over some fixed finite alphabet, then there exist indices i < j {\displaystyle i<j} i<j such that w i {\displaystyle w_{i}} w_i can be obtained from w j {\displaystyle w_{j}} w_j by deleting some (possibly none) symbols. In the classical proof, the way the indexes i,j are effetively obtained is hidden behind the use of Excluded Middle axiom and second order definitions of sets. Later in 1994, Coquand generalizes ideas from this particular case analysis in a paper "On the computational content of the axiom of choice" with S. Berardi and M. Bezem. This paper provided a general method for a constructive interpretation of classical proofs, using choice axiom and second order definitions of sets. The classical definition of a choice map is constructively interpreted as a trial-and-error mechanism, in which finite subsets of the map are proposed, tested against data, possibly rejected, and then improved according to the result of the testing. In the talk, we present this paper and we compare it with previous and later works about constructive interpretations of classical mathematics.

Ulrich Berger- Swansea UniversityExtracting concurrent programs from proofs(j.w.w. Hideki Tsuiki, Kyoto University) We present a logical system CFP (Concurrent Fixed Point Logic) that supports the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by a binary operator called restriction which strengthens implication, and a unary operator for total concurrency. The source of the extraction are formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy's amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of our system is that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb.

Marc Bezem- University of BergenSolving universe level constraintsThierry Coquand and I recently published a note in TCS with a constructive proof of the decidability of loop checking and the uniform word problem for join-semilattices with an inflationary endomorphism. In the talk I will present the polynomial algorithm that is implicit in this proof and will discuss recent experiments by Sozeau to put this algorithm to work in Coq.

Olivia Caramello- University of InsubriaRelative toposes as a generalization of localesThe aim of this talk is to present a way for representing relative toposes which naturally generalizes the construction of the topos of sheaves on a locale, and which is particularly effective for describing the morphisms between relative toposes in a concrete way. Our theoretical framework is based on the language of stacks and fibred sites, and provides, amongst other things, a unified setting for investigating the relationships between Grothendieck toposes as built from sites and elementary toposes as built from triposes.

Cyril Cohen- INRIAUnsolvability of the Quintic Formalized in Dependent Type Theory(j.w.w. Sophie Bernard, Assia Mahboubi, Pierre-Yves Strub) In this talk, we describe an axiom-free Coq formalization that there does not exists a general method for solving by radicals polynomial equations of degree greater than 4. This development includes a proof of Galois' Theorem of the equivalence between solvable extensions and extensions solvable by radicals. The unsolvability of the general quintic follows from applying this theorem to a well chosen polynomial with unsolvable Galois group.

Martin Escardó- University of BirminghamnThere are more groups in the next universeAt least one of the usual proofs that "type in type" gives rise to an inconsistent system [1] can be reformulated to prove that, in the system without "type in type", there are strictly more types in the next type universe. It should also be the case that there are strictly more groups in the next universe. We formulate and prove this in a "Spartan" Martin-Löf type theory, assuming univalence and the existence of propositional truncations in the sense of HoTT/UF. In particular, we don't include higher-inductive types other than propositional truncation, or propositional resizing axioms. In order to achieve this, we work with ordinals in the sense of the HoTT book, and with an explicit construction of free groups due to Mines, Richman and Ruitenburg (1988). We then consider the group freely generated by the large type of all small ordinals. But this is not enough. In this talk we explain what else is needed and how to accomplish it. This is joint work with Marc Bezem, Thierry Coquand and Peter Dybjer. A preprint is not available yet, but there is literate Agda code available: https://www.cs.bham.ac.uk/~mhe/TypeTopology/BuraliForti.html [1] Thierry Coquand, The paradox of trees in type theory. BIT Numerical Mathematics, March 1992, Volume 32, Issue 1, pp 10–14

Xavier Leroy- Collège de FranceProgramming in type theory, or: how Coq became my favorite programming languageThis talk will try to give a functional programmer's perspective on some of Thierry Coquand's work. The Calculus of Inductive Constructions, as implemented in the Coq proof assistant, is not just a powerful logical system, but also a surprisingly capable programming language, much more usable than the Curry-Howard correspondence lets you expect. I will discuss the joys and sometimes the pains of "hyper-pure" functional programming in Coq, based on my experience developing and verifying the CompCert optimizing compiler. One of the difficulties I encountered is that algorithmically-efficient data structures raise delicate issues with equality and with efficient evaluation of data containing proof terms. I keep hoping that homotopy type theory, or at least observational type theory, can provide principled yet practical approaches for the efficient execution of this kind of dependently-typed programs.

Assia Mahboubi- INRIAFormalizing mathematics, in practiceIn the course of the last decade, interactive theorem provers based on the calculus of inductive constructions (CIC) have attracted a growing number of users motivated by formalizing a broader spectrum of mathematics. Recent results, contemporary mathematics or even proofs in the making have been implemented as digital libraries of formally verified mathematics, in CIC. This talk will try to give an overview of this flurry, with a personal emphasis on some features which contribute to the success of this formalism, for to purpose of formalizing mathematics in practice.

Anders Mörtberg- Stockholm UniversityFormalizing π₄(𝕊³) ≃ ℤ/2ℤ and computing a Brunerie number in Cubical AgdaIn his 2016 PhD thesis Guillaume Brunerie gave the first synthetic proof in Book HoTT of the classic result that π₄(𝕊³) ≃ ℤ/2ℤ. The proof is one of the most impressive pieces of synthetic homotopy theory to date and uses lots of advanced classical machinery. Furthermore, the proof is fully constructive and the result can be formulated as "there exists an integer 𝛽 such that π₄(𝕊³) ≃ ℤ/𝛽ℤ". Using cubical type theories the hope was that this "Brunerie number" should be directly computable using a computer, but this turned out to be a computationally very hard problem. Thierry was involved in one of the first attempts to compute this number using the first cubical prototype already in 2014 and since then countless attempts using increasingly powerful computers and cubical systems have failed. However, in the last year me and my student Axel Ljungström have found some major simplifications to Brunerie's original proof, making it possible to finally compute a Brunerie number using Cubical Agda in a matter of seconds.

Stefan Neuwirth - Université Bourgogne-Franche-ComtéThierry Coquand and Paul LorenzenMy collaboration with Thierry started with a study of Lorenzen's work in logic and algebra that is still ongoing. I shall present this study with a focus on the rôle played by constructivity in the work of the two and how their conceptions respond to each other.

Andrew Pitts- University of CambridgeThierry Coquand and Constructive Type Theory -- a personal perspectiveIn this talk I will discuss which of Thierry Coquand's many contributions to the theory and applications of constructive type theory are the ones that I most value. I will survey the current state of Type Theory from this perspective and highlight some aspects where I think there is room for improvement.

Peter Schuster- University of Verona Between transfinite and dynamical proof methods (j.w.w. Daniel Wessel) The dynamical proof method was developed to make sense in constructive mathematics of the numerous instances of the axiom of choice modern algebra abounds with. Recently the dynamical method has proved to reach into general algebra, and thus to cover more universal transfinite proof principles. This prompts the question whether dynamical methods vindicate their transfinite forerunners a century after, on top of substituting them well for computation. Technically, a key role is played by an inductive generalisation of the Jacobson radical membership to which amounts to termination of generation trees. As for dynamical algebra proper, the ideal objects postulated by the transfinite methods are approximated by paths in finite binary trees which proceed at branchings as if they actually were ideal objects.

Helmut Schwichtenberg- LMU MunichVerified algorithms via proofs (j.w.w. Nils Koepp)Real numbers in [0,1] can be represented by streams of digits 0,1. Algorithms operating on such streams can be extracted from formal proofs involving a unary coinductive predicate CoI on (standard) real numbers x: a realizer of CoI(x) is a stream representing x. We address the question how to obtain bounds for the look-ahead of such algorithms: how far do we have to look into the input streams to compute the first n digits of the output stream? We present a proof-theoretic method how this can be done. The idea is to replace the coinductive predicate CoI(x) by an inductive predicate L(x,n) with the intended meaning that we know the first n digits of a stream representing x.

Bas Spitters- Aarhus UniversityA comparison of topological toposes (j.w.w. Martin Bidlingmaier)Several people have observed that there is a similarity between the three toposes: Pyknotic sets, Johnstone's topological topos and the Escardo-Xu topos. We will explore how they are similar and how they are different. We study their connection to homotopy type theory. We will conclude with some open questions.