Coq is a programming language: have you ever dreamed of using it to program itself? Even better, to certify said programs? MetaCoq does just that (and much more). Let's have a tour together!

If you want to play around live, I recommend installing the coq-metacoq-template opam package beforehand, and to check that you can step through this file: https://github.com/MetaCoq/tutorials/blob/main/popl24/exercises/MetaCoqPrelude.v

At the heart of homotopy type theory (HoTT) is the analogy between types and spaces. This analogy invites us to repurpose the methods of algebraic topology, such as homology and cohomology, for the study of types and functions between them.

In this talk, we will look at the classical theory of CW complexes and investigate which parts can be reproduced constructively in type theory. In particular, we will focus on the cellular approximation theorem, the Hurewicz theorem, and the use of cellular homology to compute homology groups.

This is joint work with Axel Ljungström and Anders Mörtberg.

Unreachability is a property at the heart of garbage collection: if a location is unreachable, it can be safely deallocated. However, formally reasoning about unreachability is challenging. Indeed, to prove that a location is unreachable, one has to consider the whole heap and possibly multiple concurrent stacks, making local reasoning apparently out of reach. In this talk, I will present two projects tackling the challenge of unreachability.

In the first part, I will present my PhD thesis work: an Iris-fueled Separation Logic with space credits, allowing for the verification of heap space bounds in the presence of concurrency and garbage collection. Crucially, this logic tracks the reachability of heap objects in a modular way, and allows for recovering space credits when the user proves an object unreachable.

In the second part, I will present another line of work about disentanglement. Disentanglement is a property of parallel programs asserting that a location allocated by a task must remain unreachable by concurrently executing tasks. Making use of disentanglement, the MPL (MaPLe) compiler for parallel ML equips programs with a blazingly fast, task-local, garbage collector. I will present DisLog, an Iris-fueled Separation Logic for verifying disentanglement, and present ongoing work on TypeDis, a type system for automatically verifying disentanglement.

The jsCoq project enables users to embed Coq code and run Coq directly within a webpage, facilitating interactive formal documents using only a modern browser.

jsCoq began in 2015 as an experiment to test the js_of_ocaml compiler, later evolving to offer an install-free distribution of math-comp proofs in a convenient presentation format.

The combination of a) an install-free Coq setup, b) full-featured package manager with many contributions available, and c) a literate programming format made jsCoq quite popular within the Coq teaching community.

However, the first jsCoq implementation had several limitations in terms of usability, document expressiveness, and constraints inherent to Coq’s standard document manager, the STM.

Work began in 2016 to replace the STM with a model better suited for jsCoq's rich document model and usability needs, culminating in 2022 with Flèche, a new document manager for Coq specifically designed to accommodate jsCoq use cases.

In this talk, we will introduce jsCoq 2, a major update to the jsCoq based on Flèche and the coq-lsp language server.

jsCoq 2 offers a continuous interaction model better suited for teaching and directly supports rich, jsCoq-style documents. This update addresses many technical challenges and enables users to develop courses and interactive documents entirely in the browser, using different editors, including rich WYSIWYG ones.

We will discuss the context and design requirements behind jsCoq and Flèche, providing a detailed overview of jsCoq 2's main features, novelties, and future roadmap.

jsCoq 2 is joint work with Shachar Itzhaky (Technion - Israel Institute of Technology).

There are many ways to teach proof competence. Students try to use “perfect” proofs from textbooks or experts to create their own proofs in exercises, and they often fail. In particular, many students struggle with properly understanding the structure of proofs. We believe that—for the education of Computer Science students who are used to programming—it is natural to use proof assistants to learn to develop and write proofs. In addition, the immediate feedback from proof assistants helps students to check their proofs for correctness and completeness.

However, proof assistants are not made for beginners. Moreover, learning formal and mathematical language at the same time is often overwhelming. We develop the web interface ProofBuddy based on the proof assistant Isabelle as a tool that (also) targets for beginners. We chose Isabelle, because we assume that the proximity of its Isar language to natural/mathematical language supports the learning process. Pedagogically, we experiment with a setting in which students constantly switch between pen-and-paper-proofs and their formal counterparts. ProofBuddy is designed to support this back-and-forth approach.

In the talk, I report on the architecture and the user interface of ProofBuddy, give a short introduction to Isar within ProofBuddy and present our pedagogical approach.

The idea of (constructive) reverse mathematics is to identify natural (sub-classical) axioms that are equivalent to certain mathematical theorems and therefore characterise their logical strength. Especially in the constructive case, this research programme highly depends on the choice of base theory, for which we employ the calculus of inductive constructions, and benefits from mechanisation, for which we use the Coq proof assistant.

In this talk, I will give an overview of some ongoing projects concerning Gödel's completeness theorem for first-order logic, the related Löwenheim-Skolem theorems, as well as Post's problem concerning the existence of a semi-decidable yet undecidable Turing degree strictly below the halting problem. Especially the latter exploits a synthetic approach to computability theory available in any constructive foundation, where the reference to an explicit model of computation can be disposed of by simply considering every function to be computable.

We give a short introduction to the Max-Atom Problem and its connection to type theory. Then we generalize to join-semilattices with an inflationary endomorphism and we explain how this generalization can be reformulated with Horn clauses (using an idea of Lorenzen). The key problems connected to universe polymorphism in type theory can now be formulated as loop checking problems and uniform word problems for this kind of lattices. Both can be solved by the computation of least Herbrand models of the corresponding Horn clauses.

In the second half of the talk we propose a type theory with explicit universe polymorphism, featuring level-indexed product types and constraint-indexed product types. In this type theory, loop checking and uniform word problems in the above mentioned lattices play a crucial role.

Efficiency and complexity issues will briefly be addressed throughout the talk. The research presented here is joint work with many people: Nieuwenhuis, Rodríguez-Carbonell, Coquand, Dybjer, Escardó.

Parametricity was introduced by Reynolds as a way to prove abstract uniformity properties for polymorphic functions. Initially, this was done externally, but recent works by Bernardy and Moulin have shown how to develop a dependent type theory that can prove these results internally. Such a theory could form the basis of a proof assistant with parametricity's uniformity properties. Unfortunately, the presheaf model of internal parametricity in the third paper of Bernardy and Moulin's series on internal parametricity contains flaws that need to be addressed. This observation will serve as a pretext for this talk to introduce the subjects of dependent type theory and (internal) parametricity.

One remarkable feature of humans is that they exhibit intrinsically-motivated behavior, partaking in activities for their own sake. This is a crucial facet of learning across all ages as well as a distinctive feature of art, science and innovation. In this talk, we will present some computational approaches seeking to emulate this process using state-of-the-art machine learning techniques as a backbone. We will first begin by surveying the field of open-ended learning and notably the concept of autotelic agents – agents that learn by inventing and pursuing their own goals. We will then present two recent works along those lines. The first is an iterative autotelic algorithm for generating a diverse set of challenging Python programming puzzles, inspired by recent advances in language-model based evolutionary computation. The second is an ongoing research project for building autotelic mathematical agents coupled to interactive theorem provers. The general design of such an agent will be given along with some motivating examples and discussion of current art. We will then present preliminary results with one important component of this agent: a theorem search engine in Lean 4, allowing one to retrieve lemmas and theorems with natural language queries.

Il est connu que les topos élémentaires ont la force logique de la logique d'ordre supérieur HOL, c'est-à-dire la force logique du système Fω. Plus concrètement, Lambek caractérise la logique des topos élémentaires comme étant une variante intuitionniste de HOL, incluant extensionnalité des propositions, extensionnalité des fonctions et axiome du choix unique. Pour chacun de ces ingrédients, et y compris pour son cœur logique qu'est Fω, on sait moralement associer un contenu calculatoire, mais où se cache-t-il dans la définition de topos élémentaire ? C'est le genre de questions qu'on se posera mais sans avoir toutefois toutes les réponses encore.

En tout cas, on commencera par voir le classificateur de sous-objet comme un hProp imprédicatif, par isoler le rôle de l'extensionnalité des propositions (= univalence pour hProp) dans la correspondance entre représentations fibrées et indexées des prédicats dans les topos, et par comprendre comment la somme disjointe peut se simuler en combinant le pouvoir de décision de la définition imprédicative de la disjonction avec le pouvoir de représentation des types par des parties singleton.

Tactician is a proof synthesis platform that aims to make machine learning models practically accessible to Coq end-users. To this end, it makes a wide range of Coq's internal knowledge available to solving agents in a machine-learning friendly manner, including information on definitions, theorems and proofs. When the user invokes Tactician's 'synth' tactic, the solving agent is asked exploit this knowledge to complete the current proof. A wide variety of solving agents are available in the platform, including k-nearest neighbor solvers, graph neural networks, language models and random forests. Several solvers have state-of-the-art proving capabilities, far outperforming existing general purpose automation techniques. Much of this performance is due to Tactician's unique capability to learn from new knowledge on-the-fly. It can amend its models with new definitions, lemmas and proofs and immediately exploit this information during proof synthesis.

In this talk, I will give a general tutorial on Tactician. We start with a usage demonstration from an end-user perspective. Then we'll take a look at Tactician's internal architecture. There are several data formats for machine learning, including a novel graph-based representation of the Calculus of Existential Inductive Constructions, where every node in the graph represents a unique term modulo alpha-equivalence. This data is made available both as an offline dataset and through interaction with Coq using a rich remote procedure calling (RPC) protocol. We'll see how we can easily implement our own external solving agent in Python.

“Fuzzing” is a popular testing approach where we throw random inputs at a program and check that it respects some expected properties on all inputs. Fuzzing a metaprogram such as a compiler requires producing random input programs. To exercise interesting behaviors of the compiler, we want our input programs to be well-formed in a strong sense, in particular to be well-typed. Generating random well-typed program is difficult when the type-system is powerful, there is a whole scientific literature on the topic, see for example [Testing an Optimising Compiler by Generating Random Lambda Terms, Pałka, 2012].

Most existing generators integrate a large part of the implementation of a type-checker, “inverted” to assist in top-down random term generation by efficiently discarding choices that result in ill-typed programs. Scaling this approach to a full language would result in implementing two sophisticated type-checkers, once in the compiler and once in the program generator. This is one type-checker too many!

In this talk I will present preliminary work on reusing the constraint-based type inference approach [The Essence of ML-based type inference, Pottier and Rémy, 2004] to write a single type-checker that can be used for both purposes: to check types of user-provided programs, and to efficiently guide a random program generator. This only requires a fairly simple modification to constraint generators: parametrizing them over a search monad.

(Relevant previous work is [Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System, Fetscher, Claessen, Pałka, Hughes, Findler]. They start from Redex, a Racket DSL to implement simple type systems, and derive a random program generator. The limitation of this approach is that Redex only works with fairly simple type system, in particular we do not expect it to scale to ML-style type inference with polymorphism, which is the part that hand-crafted generators also struggle on. Our work builds on top of constraint-solving approaches that are known to scale well to ML-style polymorphic; but it is preliminary and we have only implemented support for the simply-typed lambda-calculus for now.)

Synchronous languages are now a standard industry tool for critical embedded systems. Designers write high-level specifications by composing streams of values using block diagrams. These languages have been extended with Bayesian reasoning to program state-space models which compute a stream of distributions given a stream of observations. Yet, the semantics of probabilistic models is only defined for scheduled equations – a significant limitation compared to dataflow synchronous languages and block diagrams which do not require any ordering.

In talk I will present two schedule agnostic semantics for a probabilistic synchronous language. The key idea is to interpret probabilistic expressions as a stream of un-normalized density functions which maps random variable values to a result and positive score. The co-iterative semantics extends the original semantics to interpret mutually recursive equations using a fixpoint operator. The relational semantics directly manipulates streams and is thus a better fit to reason about program equivalence. We use the relational semantics to prove the correctness of a program transformation required to run an optimized inference algorithm for state-space models with constant parameters.

This is joint work with Louis Mandel and Christine Tasson.

In this talk, we will present a quick overview of our work (with Michael Beeson, Pierre Boutry, Gabriel Braun and Charly Gries) about formalization of geometry and the GeoCoq library. We will delve into the axiomatic systems of influential mathematicians such as Euclid, Hilbert and Tarski and present formalization issues. A special focus will be placed on the formalization of continuity axioms and parallel postulates. We will highlight details and issues that can be seen only through the lens of a proof assistant and intuitionistic logic. We will present a syntactic proof of the independence of the parallel postulate. From axiomatic foundations to computer-assisted proofs, we will explore the interplay between synthetic and analytic geometry, and different kinds of automation. Finally, we will present our recent work on Larus (with Predrag Janičić): a theorem prover based on coherent logic and constraint solving which can output proofs that are both readable and machine checkable, along with illustrations generated semi-automatically.

Contrarily to Girard's linear logic which is equipped with a rich proof theory, Kozen's modal mu-calculus has an underdeveloped one: for instance the modal mu-calculus is lacking a proper syntactic cut-elimination theorem.

During this talk, I will present a strategy to prove cut-elimination theorem for the modal mu-calculus. This strategy is to prove cut-elimination for a “linear translation” of the modal mu-calculus (that is to define a translation of the statements and proofs of the modal mu-calculus into a linear sequent calculus) and to deduce the desired cut-elimination results as corollaries.

While designing this linear translation, we come up with a sequent calculus exhibiting several modalities (or exponentials). It happens that the literature of linear logic offers tools to manage such calculi, for instance subexponentials by Nigam and Miller and super exponentials which is a work I did with Olivier Laurent.

We actually extend super exponentials with fixed-points and non-wellfounded proofs (of which the linear decomposition of the modal mu-calculus is an instance) and prove a syntactic cut-elimination theorem for these sequent calculi in the framework of non-wellfounded proof theory.

Back to the classical modal mu-calculus, we deduce its cut-elimination theorem from the above results, investigating both non-wellfounded and regular proofs.

This is a joint work with Alexis Saurin.

1. [Premier exposé : Micaela] Title: An overview of the real numbers in theorem provers: an application with real analysis in Coq

Abstract: Formalizing real numbers in a formal proof tool represents a particular challenge. It is not only a question of representing numbers in computers but also of preserving all mathematical properties needed to make proofs. We will review the history of real numbers formalization in different proof assistants and the different ways of formalizing them, before giving an overview of real numbers libraries that exist today in provers. As application, we will finish by presenting real analysis developments in Coq.

2. [Deuxième exposé : Houda] Title: Formal proofs in applied mathematics: Formalization of Tonelli Theorem and Lagrange Finite Elements

Abstract. Numerical analysis, as an essential tool for solving complex mathematical problems through the use of algorithms and numerical approximations, is further fortified in this work by rigorously formalizing Tonelli's Theorem and Lagrange Finite Elements. These basic concepts are defined and validated using formal proof techniques, enhancing their credibility in various mathematical applications. In the field of integration, important results such as Tonelli's Theorem and the Lebesgue Induction Principle are covered. Furthermore, in the field of numerical resolution of partial differential equations, we explore finite elements, covering the general definition of finite elements, and geometric transformations, up to the full definition of simplicial Lagrange finite elements, including the unisolvance property.

Observational Type Theory is an internal language for types equipped with a proof-irrelevant propositional equality. As such, it natively supports extensionality principles, UIP, and quotients of types by proof-irrelevant relations (à la Lean).

Unfortunately, it is difficult to use these quotients without any choice principles to extract information from proof-irrelevant truncations. In this talk, I will discuss the various choice principles one could hope to have in OTT, and I will use ideas from Higher Observational Type Theory to sketch a version of OTT with unique choice.