CIRM 2025: Tentative schedule

Monday
proofs and synthetic mathematics
09:15
10:10
Break
10:40
11:10
Benno van den Berg
Constructive ordinals
11:40
12:20
Break
12:30
Lunch
14:30
16:00
16:50
17:20
Break
17:40
18:10
18:40
Break
19:30
Dinner
Tuesday
categories
09:15
10:10
Break
10:40
11:30
12:00
Group picture
12:30
Lunch
14:30
16:00
16:40
Break
17:10
18:00
18:30
19:00
Break
19:30
Dinner
20:45
Wednesday
set-theoretic realizability
09:15
10:10
Break
10:30
11:00
11:40
12:10
12:20
Unallocated/Buffer
12:30
Lunch
19:30
Dinner
20:45
21:15
Thursday
types, realizability and algebra
09:15
10:10
Break
10:40
11:30
12:20
Unallocated/Buffer
12:30
Lunch
14:00
14:35
Unallocated/Buffer
14:50
15:30
16:20
17:10
Break
17:40
18:10
19:00
Break
19:30
Conference dinner
20:45
Evening session
Slideshow on the patio
23:00
Evening session
Night hike
Friday
more tantalizing topics
09:10
09:40
10:10
Break
10:25
11:05
11:55
12:25
Unallocated/Buffer
12:30
Lunch
19:30
Dinner
Working groups are an addition to the official conference program. The first five Tuesday talks will be recorded by CIRM staff. PDF version of the schedule

Proposals for working groups or evening talks

Please express your interest to these people:

Joost Joosten: Efficient proof systems in provability logics

See here (PDF)

Benno van den Berg: Constructive ordinals

The notion of a well-order is one of the fundamental notions of logic, both in a classical and a constructive setting. So one would expect the notion of ordinal, as a canonical representative of an isomorphism class of well-ordered sets, to play a prominent role in both contexts.

Where the classical theory is well-established, the constructive picture is more confusing. At least, I thought so not too long ago. But upon closer inspection I feel there is actually a pretty clear picture emerging, supported by ideas from constructive set theory, homotopy type theory and algebraic set theory. The goal of this talk is to say what this picture is. For this, I will focus on transfinite iteration as the "killer app"" of the theory of ordinals (and the reason Cantor invented it), and also discuss some issues going forward.

Slides

Peter LeFanu Lumsdaine: Richer type theories for arithmetic universes

Categorical settings for finitistic mathematics are given by Joyal’s arithmetic universes — list-arithmetic pretoposes, to be specific — and their siblings locoses — list-arithmetic lextensive categories. Maietti and others have introduced type theories for these, allowing working conveniently with their core structure of lists, pair types, equality types, etc.

These form a suitable foundation for finitistic mathematics, by encoding arbitrary finite objects as numbers/lists. Obviously, though, one wants to avoid handling such encodings explicitly, as far as possible.

This motivates setting up a much richer type theory, motivated by expressivity rather than economy, presenting further constructions ubiquitous in the practice of finitistic mathematics: a universe of finite sets; finitary exponentials; and finitary inductive types. The usual list-encoding techniques then show that this is conservative over the core type theory of AU's/locoses.

Slides

Milly Maietti: Reconciling Brouwer's continuity principles with effectiveness

It is well known that Brouwer's continuity principles, implying the Fan theorem, are inconsistent with the Church thesis over Heyting arithmetic with finite types.

We show that the predicative and constructive Minimalist Foundation, for short MF, formalized in [3] according to [2], is consistent with Brouwer's continuity principles and a restricted form of the Church thesis, called the "type theoretic Church thesis" (TCT), with a predicative and constructive model.

Thanks to the results in [3] and [4], we extend the consistency proof to the impredicative Coquand-Huet's Calculus of Constructions, CC.

We conclude by observing that the consistency of TCT with Brouwer's continuity principles is a peculiar property of MF and CC among the most relevant foundations for mathematics available in the literature, since it is due the presence in them of a notion of type-theoretic function not identified with the usual notion of functional relation.

[1] Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48 in Oxford Logic Guides, p. 91-114. Oxford University Press (2005)
[2] Maietti, M.E.: A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic 160(3), 319{354 (2009)
[3] M. E. Maietti, P. Sabelli. Equiconsistency of the Minimalist Foundation with its classical version. Annals of Pure and Applied Logic, 2024
[4] M. E. Maietti, P. Sabelli., D. Trotta. "Effectiveness and Continuity in Intuitionistic Quasi-toposes of Assemblies", submitted.

Slides

Han Gao: A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels

The logic IK is the intuitionistic variant of modal logic K and is considered a fundamental intuitionstic modal system. In this talk we present a labelled-free bi-nested sequent calculus for IK. This proof system comprises two kinds of nesting, corresponding to the two relations of bi-relational models for IK: a pre-order relation, from intuitionistic models, and a binary relation, akin to the accessibility relation of Kripke models. The calculus provides a decision procedure for the logic by means of a suitable proof-search strategy. This is the first labelled-free calculus for IK which allows direct counter-model extraction: from a single failed derivation, it is possible to construct a finite countermodel for the formula at the root.

Slides

Felix Cherubini: The abelian closure of finite free modules in synthetic algebraic geometry

This is joint work in progress with Dan Christensen and Thomas Thorbjørnsen.

Over some commutative rings the category of finitely presented modules is abelian. This happens to fail for the base ring R in synthetic algebraic geometry, a conjectural internal language of a higher Zariski topos, given by homotopy type theory extended by three axioms.

It was already discovered in work on the differential geometry of synthetic schemes that the categories of finitely presented modules and finitely co-presented modules are anti-equivalent. We will give a sketch of a proof that the category of images of maps from finitely co-presented to finitely presented modules is abelian and self-dual. This work is part of an attempt to prove a synthetic version of Serre-Duality.

Freek Geerligs: Synthetic Stone duality

Synthetic Stone duality is a variant of synthetic algebraic geometry, which extends homotopy type theory with 4 axioms. We introduce notions of closed and open propositions. These give a synthetic topology on any type. In this topology, any map is continuous. We are particularly interested in Stone and Compact Hausdorff spaces, where the synthetic topology is as expcected. In particular, any function from the interval to itself is continuous in epsilon-delta sense. We also decide Bishop's omniscience principles with our axioms.

This talk is based on https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3

Hugo Moeneclaey: From synthetic Stone duality to synthetic algebraic topology

In this talk we will explain joint work with Felix Cherubini, Thierry Coquand and Freek Geerligs. We want to use synthetic Stone duality as a framework to do algebraic topology. Indeed, this setting allows for synthetic approaches to both topology (see Freek Geerligs talk) and homotopy (as an extension of HoTT), so it is a natural candidate for doing synthetic algebraic topology.

To give an example, we have the topological circle defined as the type of reals x and y such that x^2+y^2=1, which is a 0-type with an interesting topology. On the other hand, we have the homotopical circle defined as the higher inductive type generated by a loop, which is a 1-type with trivial topology. In synthetic Stone duality, we can relate them using the shape modality, which is simply defined as the nullification at the unit interval. The shape of a topological space is its corresponding higher groupoid. This is analogous to what happens in real cohesive homotopy type theory, except we are working from axioms instead of introducing a comodality.

In this talk we will only consider cohomology with coefficient in countably presented abelian groups. We will introduce Barton-Commelin axioms, which can be proven in synthetic Stone duality and immediately implies that maps from a compact Hausdorff space to a countably presented abelian group are well-behaved. From these we will explain how:

1) Stone spaces are acyclic.
2) The cohomology of compact Hausdorff can be computed using Cech cohomology.
3) The unit interval is acyclic.
4) The shape of a countable topological CW complex is the expected countable homotopical cell complex (assuming hypercompletness).
5) The cohomology of countable topological CW complex is as expected, despite them being sets!

All the axioms of synthetic Stone duality follow from choice for sets, except the one stating that all maps between Stone spaces are continuous. We find it striking that this continuity principle implies these results on the cohomology of sets.

Quentin Schroeder: Mnemetic Monads and Compactness

Lax-idempotent monads on 2-categories encode notions of cocompletions. We will show an abstract condition to characterize a notion of compactness that comes with each such lax-idempotent monad. Familiar examples include: the down-set monad giving rise to completely join-prime elements, the Ind-completion giving rise to finitely presented objects and the ex/lex completion giving rise to projective objects in the sense of homological algebra.

The condition will be stated in terms of the category of algebras of the lax-idempotent monad T, namely a morphism is "T-compact" when it satisfies a certain 2-categorical universal property with respect to the structure of the monad.

We then state that taking compact objects is right adjoint to taking free continuous algebras. Thus giving an abstract account of certain equivalences arising from Stone Duality and Categorical Logic.

Emily Riehl: Synthetic perspectives on the Yoneda lemma

The Yoneda lemma, considered to be the fundamental theorem of category theory, is difficult to explain because its statement is both abstract and obscure. But in synthetic category theory, "functionality" and "naturality" are automatic, and the Yoneda lemma can be understood as an "arrow induction" principle that applies in covariant or contravariant settings.

This is based on joint work with Mike Shulman that can be understood as prerequisites for more recent work of Weaver, Licata, Weinberger, Bardomiano Martinez, Gratzer, Buchholtz, and others.

Alex Simpson: Synthesising random variables

In a longstanding and still ongoing research project, I have been developing a synthetic approach to probability theory based on axiomatising a primitive notion of random variable. In this talk, I shall discuss the process of developing of the axiomatisation, touching on various considerations that influenced the choice of axioms, the current state of the theory, and lessons learned from the process so far.

Jacopo Emmenegger: Towards the effective 2-topos

Hyland's effective topos Eff models extensional type theory with an impredicative universe of propositions, as it does any (elementary) topos. Remarkably, it contains another impredicative universe which turns out not to be a poset, that of so-called modest sets. This fact ensures that Eff also models type theories like System F and the Calculus of Constructions. Impredicative encodings of type constructors, while very economical, often fail to satisfy a certain uniqueness principle (the so-called eta-rules) and, in turn, do not have dependent eliminators and thus do not support proofs by induction. Awodey, Frey and Speight have shown how to use a univalent impredicative universe to produce encodings that do enjoy (propositional) eta-rules and dependent eliminators. It is then natural to look for a semantic setting where to carry out such encodings. Current approaches to higher versions of Eff often take simplicial or cubical sets inside Eff or inside its subcategory of assemblies. It was shown, however, that the subcategory of 0-types (the sets) in these higher toposes is not Eff. I will present work in progress with Steve Awodey where we construct a candidate effective 2-topos that does contain Eff as its subcategory of 0-types. An infinity version of this construction is being investigated by Anel, Awodey and Barton.

Slides

Sophie d'Espalungue: Towards an internal construction of meaning

I will share ideas underlying an internal approach I am developing to address the notion of meaning in mathematical language. I’ll outline some expected benefits and explore how the syntax-semantics and analytic-synthetic dichotomies would fit into this framework.

The idea is to organise mathematical objects and structures into a nested hierarchy, each level internalising the level below. The fundamental instance corresponds to the hierarchy of n-categories (proof of true, true, truth values, sets, categories, etc.)

Given that this hierarchy includes the level of truth values, this approach further seeks to internalise the process of definition by formulating it at that very level, blurring the line between syntax and semantics. In this framework, no term is primitive: each object is defined as an element of an object at the next level up, built inductively from the levels below.

The aim is to explore how meaning can emerge internally from the act of definition itself. My goal in this talk is to present this perspective, clarify intuitions, and invite discussion on its mathematical and philosophical implications.

Slides

Ulrik Buchholtz: Towards synthetic locale theory

In synthetic mathematics, we often pick a particular topos (say, a classifying topos for a nice theory), and work in the internal language of its (higher) sheaves. But to reap the full benefits of a synthetic statement we need to externalize and connect the internal with the external world. In my talk, I'll explore approaches to giving a synthetic account of (iterated) internalization. One is ongoing work by David Jaz Myers and Mitchell Riley on “theory type theory”, and another is “geometric type theory” as advocated by Steven Vickers.

Both of these require radical new type theories, which in the long term is surely the right way to go. Here, we propose a simpler account, where we use type theory as is to build a “synthetic mathematics for synthetic mathematics”, inspired by Blechschmidt's duality axiom as arising from (large) sheaves on the category of small locales and small maps.

This can be seen as a next step in a sequence of synthetic theories exploring more and more structure on locales, based on what kind of observations are axiomatized.

El Mehdi Cherradi: Internal languages of locally cartesian closed (∞,1)-categories

We establish a DK-equivalence between the relative category of π-tribes and the relative category of locally cartesian closed quasicategories. From this follows one of the internal languages conjecture: Martin-Löf type theory with dependent sums, intensional identity types, and dependent products satisfying function extensionality is the internal language of locally cartesian closed (∞,1)-categories.

Slides

Jonathan Weinberger: Universes in synthetic (∞,1)-category theory

To reason synthetically about ∞-categories, Riehl and Shulman introduced a simplicial extension of HoTT in 2017. This allows for the development of important ∞-categorical concepts such as adjunctions, (co)limits, and fibrations, some of which have been formalized in Kudasov's proof assistant Rzk.

However, for a long time the theory had been missing categorical universes such as the ∞-category of (small) ∞-categories or ∞-groupoids, resp. We present the construction of these universes in a modal extension of simplicial HoTT, showcasing some applications to higher algebra.

The formalization is joint work with Nikolai Kudasov and Emily Riehl. The work on universes is joint with Daniel Gratzer and Ulrik Buchholtz.

Slides

Mohamed Barakat: CAP — a categorical (re)organization of computer algebra

In this talk I will introduce CAP (Categories, Algorithms and Programming), an open-development multi-package software project for algorihmic category theory. CAP is currently loosely organized by the category of doctrines. By a "doctrine" we mean a 2-category of structured categories (including various monoidal categories), structure-preserving 2-functors, and natural transformations between them. Compositions of such 2-functors applied to a specific category give rise to what we call "categorical towers", a highly economic and modular way to create various computational contexts in computer algebra. Such modular code cannot be optimized by hand for comptutational performance as it would require breaking the modularity: Each layer in the tower treats the layer below merely as a blackbox. This forced us to develop CompilerForCAP, a category-theory-aware compiler that is able to get rid of the entire categorical abstraction and produce efficient low-level code which is almost impossible to write by hand, let alone error-free.

Slides

Ryota Kuroki: A quantitative Hilbert's basis theorem and the constructive Krull dimension

See here (PDF)

Slides

Gabriele Buriola: A constructive picture of Noetherian conditions and well quasi-orders

From a constructive perspective the many notions of Noetherianity and well quasi-order form a rich landscape, which we here explore. Besides the well-studied conditions about sequences, we include the finite basis property of the original Higman lemma, trying a first joint analysis of Noetherianity and well quasi-order in the spirit of reverse mathematics with intuitionistic logic.

Slides

Pierre-Marie Pédrot: > implying implications can go another direction

In this talk, we will describe a Dialectica interpretation of Martin-Löf Type Theory as a syntactic model. It includes all fancy features of dependent types such as dependent elimination and universes. Contrarily to effectul models, Dialectica does not change the interpretation of values, but instead of functions. It enriches usual "forward" functions with an additional "backward" component, which can be seen as a trace of evaluation of the former. We will argue that this backward feature gives to a generalization of graded types to a very expressive setting where annotations range over complex higher-order objects rather than just elements of a semi-ring, paving the way to a type theory for synthetic complexity.

Slides

Étienne Miquey: Generic approaches to effectful realizability

Constructive foundations have for decades been built upon realizability models for higher-order logic and type theory. However, traditional realizability models have a rather limited notion of computation, which only supports non-termination and avoids many other commonly used effects. Nonetheless, many recent works have shown how realizability models could benefit from side effects to provide computational interpretation for logic principles. In earlier work with Cohen and Tate [1], we addressed the challenge of finding a uniform and generic algebraic framework encompassing (effectful) realizability models, introducing evidenced frames for this purpose. These structures not only enable a factorization of the usual construction of a realizability topos from a tripos—evidenced frames are complete with respect to triposes—but are also flexible enough to accommodate a wide range of effectful models.

We pursued this along two main directions:

- first, by extending the syntactic (typed) approach to realizability, following Kreisel’s tradition, where propositions from a ground logic (e.g., HOL) are translated into specifications and typed programs (realizers) that satisfy them. We introduce EffHOL [2], a new framework that expands syntactic realizability. It combines higher-kinded polymorphism—enabling typing of realizers for higher-order propositions—with a computational term language using monads to represent and reason about effectful computations.

- second, by generalizing the traditional notion of Partial Combinatory Algebras (PCAs), which underpins classical realizability models. To better internalize a broad spectrum of computational effects, we propose the concept of Monadic Combinatory Algebras (MCAs) [3], in which the combinatory algebra is structured over an underlying computational effect captured by a monad. As we shall see, MCAs provide a smooth generalization of traditional PCA-based realizability semantics.

[1] Evidenced Frames: A Unifying Framework Broadening Realizability Models. Cohen, Miquey & Tate. LICS 2021
[2] Syntactic Effectful Realizability in Higher-Order Logic. Cohen, Grünfeld, Kirst & Miquey. LICS 2025
[3] From Partial to Monadic: Combinatory Algebras with Effect. Cohen, Grünfeld, Kirst & Miquey. FSCD 2025.

Slides

Jonas Frey: Modest sets and equilogical spaces as mono-fibrational cocompletions

The characterization of realizability triposes given here relies on the fact that realizability triposes are fibrational cocompletions under existential quantification. The present talk explains the recent observation that we are in fact dealing with a cocompletion of a completion, where the two constructions are combined via a distributive law: Given a PCA A, the forgetful functor MPAsm(A) → Set from the category of modest partitioned assemblies to sets is a poset-fibration with respect to monomorphisms (injections), and we obtain the realizability tripos rt(A) by first completing this mono-fibration to a fibered poset – yielding partitioned assemblies over sets, PAsm(A) → Set – and then freely adding existential quantification. Adding existential quantification only along surjections to PAsm(A) → Set assemblies over sets (Asm(A) → Set), and adding existential quantification along surjections to the mono-fibration MPAsm(A) → Set yields Mod(A) → Set – the mono-fibration of modest sets over Set. If the PCA is total, we can descend even further and start with an iso-fibration instead of a mono-fibration. The construction of the category of equilogical spaces and related categories fits into the same framework.

Slides

Laura Fontanella: Realizability models for set theory

In the 19th century, mathematicians began to explore fundamental questions about the foundations of mathematics. This inquiry led to the development of formal logic, marked by a particular focus on axiomatic systems, from which set theory emerged as a solid foundation for all mathematics. Around the same time, the concept of computability was investigated in connection with the idea that mathematical proofs should be "computable." This line of inquiry gave rise to Kleene's realizability.

In this talk, we will examine how these two research traditions are now converging in the field of classical realizability for set theory. We will explore the construction of models of ZF using lambda-terms and use this technique to investigate the computational content of set theory. We will present the current state of the art alongside several open problems in this area. In particular, we will show that while it is possible to realize even large cardinal axioms, the computational content of the Axiom of Choice remains elusive.

Slides

Jacopo Furlan: Bar induction and preservation of cardinals

The talk introduces a property of Krivine’s realizability algebras that corresponds to closure in the context of forcing, thereby ensuring the preservation of cardinals (below a fixed size) in the realizability model. This is achieved by combining specific requirements on the algebra with the bar induction operator. We will first present the main results derived from this property, followed by some examples of realizability algebras satisfying the requirements.

Slides

Yannick Forster: Synthetic computability in constructive type theory

tba

Victoria Barrett: Efficient proof systems in deep inference formalism (lightning talk)

tba

Hugo Herbelin: Cubical models of parametric type theory in indexed form

It is customary to interpret parametric or cubical type theories using cubical sets presented in the usual “fibered” form, that is as presheaves where segments have faces denoting their two endpoints, where squares have faces denoting their four sides, etc.

However the syntax of type theory is by default “indexed”, e.g. equality is usually represented not as a set of equality proofs equipped with source and target but rather as a family of equality proofs dependent over the terms whose equality is stated.

This justifies to explore alternative cubical sets models where segments are not sets equipped with faces but instead families dependent over endpoints, etc., that is models adopting the “indexed” side of the standard “fibered/indexed” correspondence.

By doing so, we get models liable to satisfy more definitional properties of the syntax.

Tom de Jong: Formalizing equivalences without tears

This will be a light expository talk in the context of homotopy type theory on two convenient techniques for proving – and formalizing – that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while the second refines this approach using the 3-for-2 property of equivalences. I will illustrate the techniques by proving a basic result in synthetic homotopy theory.

The talk will be based on my TYPES 2024 post-proceedings paper.

Ming Ng: What is a space, and why should a logician care?

The logician is familiar with the idea that filters are generalised points. Topos theorists push this idea further by asking: what is a generalised space?

This talk will focus on one such answer: LT-Topologies (“Lawvere-Tierney Topologies”). In the 1980s, Hyland introduced the Effective Topos, and showed that the Turing Degrees embed into its poset of LT-Topologies. Progress was slow until 2013, where Lee-van Oosten showed that this topological framework reveals a meaningful interaction between combinatorics and computable complexity.

In joint work with T. Kihara, we push this idea much further by introducing a game-theoretic version of Katetov’s Order. On the set theory side, this yields a new partial order on ultrafilters of    ℕ, strictly coarser than the classical Rudin-Keisler and Katetov Orders. On the computability theory side, the computable analogue of this order coincides with the usual partial order on LT-topologies.

This connection brings into focus a striking insight: structural questions in computability theory and in the combinatorics of filters on ℕ turn out to be controlled by the same underlying mechanism. We emphasise this is not just an analogy but a genuine unification: the topos theory supplies a single framework in which notions of complexity from both settings can be measured side-by-side, e.g. one can ask about the computable complexity of the Frechet filter. Depending on time, I plan to discuss the relative coarseness of the game-theoretic Katětov Order, its potential role in defining cohomology, as well as our original motivation of connecting the LT-topologies to Keisler’s Order on first-order theories.

Iosif Petrakis: Orthocomplemented subspaces and partial projections on a Hilbert space

We introduce the notion of an orthocomplemented subspace of a Hilbert space H, that is, a pair of orthogonal closed subspaces H, as a two-dimensional counterpart to the one-dimensional notion of a closed subspace of H. Orthocomplemented subspaces are the Hilbert space-analogue to Bishop's complemented subsets. To complemented subsets correspond their characteristic functions, which are partial, Boolean-valued functions. Similarly, to orthocomplemented subspaces of H correspond partial projections on H. Previous work of Bridges and Svozil [1] on constructive quantum logic is an one-dimensional approach to the subject. The lattice-properties of the orthocomplemented subspaces of a Hilbert space is a two-dimensional approach to constructive quantum logic, that we call complemented quantum logic. Since the negation of an orthocomplemented subspace is formed by swapping its components, complemented quantum logic, although constructive, is closer to classical quantum logic than the constructive quantum logic of Bridges and Svozil. The introduction of orthocomplemented subspaces and their corresponding partial projections in [2] allows a new approach to the constructive theory of Hilbert spaces. For example, the partial projection operator of an orthocomplemented subspace and the construction of the quotient Hilbert space bypass the standard restrictive hypothesis of locatedness on a subspace. Located subspaces correspond to total orthocomplemented subspaces.

[1] D. S. Bridges, K. Svozil: Constructive Mathematics and Quantum Physics, International Journal of Theoretical Physics, Vol. 39, No. 3, 2000, 503-515.
[2] I. Petrakis: Orthocomplemented subspaces and partial projections on a Hilbert space, arXiv:2508.15906v1, 2025 .

Luis Gambarte: Equivalences between categories with dependent arrows and comprehension categories

Dependent function types have sparked a multitude of categorical notions to interpret them, categories with families, type categories and comprehension categories to name a few.

These notions fall in one of two categories: Using fibred category theory or endowing each object of the category with additional structure. Categories with family arrows and dependent arrows as developed in [1] fall into the first category.

We will demonstrate how the notion of a (2-)fam-category is equivalent to the notion of a (discrete/split) comprehension category and then give the additional structure on fibrations/comprehension categories which will be equivalent to the additional structure of dependent arrows on (2-)fam-categories.

[1] Iosif Petrakis, Categories with dependent arrows, 2023, arXiv:2303.14754
[2] Luis Gambarte and Iosif Petrakis, Equivalences between categories with dependent arrows and comprehension categories, submitted, 2025

Slides

Ingo Blechschmidt: Tutorial on Agda (working group)

Agda is simultaneously a programming language and a proof language, helping us with…
✅ verifying correctness of proofs
🧮 implementing algorithms
💭 structuring mathematical thoughts
⚙️ appreciating mathematics from a computational angle
🚀 collaboratively engineering mathematical libraries In this informal working group, we will go on a guided tour of the basics of Agda. As case studies, we will either use commutativity of addition, correctness of insertion sort or a suitable spontaneous suggestion.

Transcript
Agdapad (for running Agda directly in your browser)
Let's play Agda (online course on Agda)
One of the papers of the ordinals gang (with beautiful interlinked formalization)
Uncountable ordinal numbers in Agda (by András Kovács)

Ingo Blechschmidt: Tutorial on extracting constructive content from classical proofs (working group)

This will be a hands-on session where we explore how we can extract constructive content from an outrageous classical proof making use of the transfinitary credo that every function ℕ → ℕ attains a minimum.

The technique (double negation translation followed by Friedman's nontrivial exit continuation trick) is quite general, so that interested persons can then embark on additional exercises: For instance, the slick classical proof of the finitary pigeonhole principle using the infinitary pigeonhole principle can be constructivized.

We will use Agda to help us in carrying out the technique, but no familiarity with Agda will be supposed.

Transcript (in Agda)
Rocq code (courtesy of Yannick Forster)
Exercises
Course with more details

Ingo Blechschmidt: An injection ℝ ↪ ℕ? Fun with hypercomputation (evening session)

There are more real numbers than natural numbers. Or are there? Meet the bizarre world of infinite time Turing machines, where two plus two is still four and still infinitely many prime numbers exist, but where the axiom of choice fails, where not every mathematical assertion is true or false—and where there is an injection from ℝ to ℕ.

Slides
Introduction to the internal language of toposes
Talk by Andrej Bauer (on a different topos, containg a surjection ℕ ↠ ℝ)
Seemingly impossible functional programs (blog post with a huge cult following)
Andrej Bauer: Intuitionistic Mathematics and Realizability in the Physical World

Iosif Petrakis: Coinductive well-foundedness

We introduce a coinductive version of the well-foundedness of ℕ that is used in our proof within minimal logic of the constructive counterpart to the standard least number principle. This notion of well-foundedness can be generalised.

Paper

Ingo Blechschmidt: Tutorial on (constructive) forcing (evening session)

Introduction to forcing, with an eye towards applications in constructive mathematics.

Slides
Paper (see especially Section 4)

References from the discussion with Emily:
Thursten 1, Thursten 2

Pierre-Marie Pédrot: Tutorial on unique choice and truncation (working group)

tba

Giulio Fellin, Sara Negri: Conservation for infinitary predicate logic

tba

Ingo Blechschmidt: Forcing the simplest counterexample (a case study in streamless sets) (working group)

A set X is streamless if and only if every infinite sequence of elements of X contains repetitions. In classical mathematics, the streamless sets are precisely the finite sets. Constructively, the notion of streamless set is weaker: For instance, streamless sets come without an upper bound on the number of their elements.

In this session, we will discuss how just a modicum of forcing can be used to construct explicit counterexamples: We will exhibit a set which is streamless but not finite; and two sets which are streamless but whose product is not.

In some sense, these counterexamples are the simplest possible. The presented technique is also useful for other situations.

This will be a blackboard session.

Ingo Blechschmidt: Slideshow on the patio (evening session)

tba

Unknown: Night hike (evening session)

tba
Merge requests welcome.