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 Nottingham
Investigating the Tarpeian rock : Paradoxes in Type Theory
Coquand 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 University
Algebraic type theory
A 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 Torino
On the computational content of the axiom of choice. About a paper with T. Coquand and M. Bezem
In 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 University
Extracting 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 Bergen
Solving universe level constraints
Thierry 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 Insubria
Relative toposes as a generalization of locales
The 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 - INRIA
Unsolvability 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 Birminghamn
There are more groups in the next universe
At 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 France
Programming in type theory, or: how Coq became my favorite programming language
This 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 - INRIA
Formalizing mathematics, in practice
In 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 University
Formalizing π₄(𝕊³) ≃ ℤ/2ℤ and computing a Brunerie number in Cubical Agda
In 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 Lorenzen
My 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 Cambridge
Thierry Coquand and Constructive Type Theory -- a personal perspective
In 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 Munich
Verified 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 University
A 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.