Je vais présenter la construction de complétions de Rezk “strictes”. En théorie des types homotopique, la complétion de Rezk d'une catégorie C est une catégorie univalente équivalente à C. Dans un cadre plus spécifique (les ensembles cubiques), la complétion de Rezk stricte permet de plus de conserver certaines égalités strictes (lois d'associativité et de neutralité).

Cette construction s'applique non seulement aux catégories, mais aussi aux modèles de la théorie des types. Elle permet alors de prouver la canonicité homotopique pour la théorie des types homotopique. Plus de détails peuvent êtres trouvés dans https://arxiv.org/abs/2311.05849.

(Note that the talk will be in fench.) This talk presents a constructive approach to trigonometry, fully formalized and proven in the Coq proof assistant, that avoids the use of π. Angles are defined as pairs of reals. Along the way, some classical trigonometric formulas naturally emerge. The process culminates in the definition of dividing an angle by an integer, achieved through a convergent sequence. No prior knowledge of Coq is required to understand the talk, as no Coq code appears in the slides. While the talk is given in French, the slides are in English, allowing non-French speakers with a basic understanding of French to follow along.

Large Language Models (LLMs) have proved surprisingly effective at solving a wide range of tasks from just a handful of examples. However, their lack of reliability limits their capacity to tackle large problems that require many steps of reasoning. In response, researchers have proposed advanced pipelines that leverage domain-specific insights to chain smaller prompts, provide intermediate feedback and improve performance through search. However, the current complexity of writing, debugging, tuning and maintaining such pipelines has put a bound on their sophistication.

We propose a new paradigm for programming with LLMs called oracular programming. In this paradigm, domain experts are invited to define high-level problem-solving strategies as nondeterministic programs. Such programs are reified into infinite search trees for LLM oracles to navigate. A separate demonstration language allows annotating choice points with examples, while keeping them grounded and synchronized as the associated program evolves.

In this talk, I will motivate and explain the key concepts of oracular programming. I will introduce Delphyne, a framework for oracular programming based on Python, discuss the associated tooling, and demonstrate Delphyne on a program verification case study. Hopefully, such a framework can foster research on intersymbolic AI and facilitate creative combinations of LLMs with symbolic provers.

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.

In this talk I will explore subtyping for dependently-typed languages, in particular how to tame the coherence problematics typical for subtyping in this context. This naturally leads to investigating a form of functoriality equations, which do not hold on the nose in vanilla MLTT.

I will explain how to repair this and add these extra equations in, and the proof techniques based on logical relations we need to set up to establish the good theoretic properties of the resulting type system, that we have recently formalised in Coq.

Assessing whether a program can be used in place of another is a classical problem, typically addressed through refinement relations.

The must-preorder, introduced by De Nicola and Hennessy in 1984, considers one process to be a refinement of another if every test satisfied by the former is also satisfied by the latter. In practice, this corresponds to updating the software running on a server without clients noticing any change.

In this talk I will present a new characterisation of the must-preorder for asynchronous processes which is simpler than the existing ones and generalize the standard characterization defined for synchronous processes.

Our work led to the implementation of a Coq framework. I shall discuss how we leveraged Coq typeclasses to make our theorems applicable to any Labelled Transition System (LTS) that respects Selinger's axioms for output-buffered agents.

La notion de groupe simple apparaît dans les travaux de Galois en relation avec la résolubilité par radicaux des équations polynomiales.

Je présenterai mon travail sur la formalisation en Lean de la simplicité du groupe alterné sur au moins 5 lettres qui repose sur un critère d'Iwasawa.

Ce théorème, souvent attribué à Galois lui-même, possède de nombreuses preuves, certaines assez courtes, et celle que j'ai choisie est en fin de compte assez longue.

Je tenterai de justifier pourquoi son schéma, les concepts qu'elle met en œuvre et les ramifications qu'elle offre la rendent, à mon sens, appropriée pour figurer dans une librairie de mathématiques formelles.

In this talk, I will discuss a proof-relevant Craig-Lyndon interpolation theorem for first-order LL (linear logic) that I studied after a question by Sam van Gool and Hugo Férée during Scalp anual meeting last february.

This interpolation is proof-relevant in the following sense: if π proves A ⊢ B, then we can find (i) a formula C in the common vocabulary of A and B and (ii) two proofs π1 and π2 of A ⊢ C and C ⊢ B respectively, such that π1 composed with π2 cut-reduces to π. Similar proof-relevant interpolation results for LJ and LK are obtained as immediate corollaries via usual linear translations.

I will explain how this result follows straightforwardly from the usual proof-theoretic method for proving interpolation and how the construction of a proof-relevant interpolant can be viewed as a cut-introduction procedure.

Finally, I shall discuss how to extend the above result to (a fragment of) circular proofs of linear logic with least and greatest fixed-points.

Higher Type Arithmetic (HA^ω ) is a first-order many-sorted theory. It is a conservative extension of Heyting Arithmetic obtained by extending the syntax of terms to all of System T: the objects of interest here are the functionals of “higher types”. While equality between natural numbers is specified by the axioms of Peano, how can equality between functionals be defined? From this question, different versions of HA^ω arise, such as an extensional version (E-HA^ω) and an intentional version (I-HA^ω). In this talk, we will study a specific model of I-HA^w: the model of Hereditary Recursive Operations. We will see how this model interprets a family of typed operations “quote_A : A → Nat” that associate, to a given functional of type A, the “source code” of its normal form.

Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal. We contribute with a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories.

Au chapitre 5 du fameux livre “Gödel, Escher, Bach”, D. Hofstadter introduit la fonction G suivante comme exemple de définition récursive:

  G(0)=0 puis G(n)=n-G(G(n-1)) pour tout entier n>0

Il définit également une fonction H selon le même modèle, mais avec trois appels récursifs imbriqués au lieu de deux pour G, et mentionne que cela continue ensuite, pour n'importe quel degré d'imbrication. Cet exposé est consacré à l'étude de la famille de fonctions que l'on obtient ainsi. Je parlerai de leurs liens intimes avec (au moins!) des arbres rationnels infinis, des variantes des nombres de Fibonacci et leur systèmes de numération associés, des mots morphiques, des nombres de Pisot, des fractales de Rauzy. Je présenterai également le développement Coq correspondant, certifiant presque toutes les propriétés en question, y compris une conjecture OEIS concernant H. Cela m'a amené à considérer en Coq des réels, complexes, polynômes, matrices, etc, ce qui est encore loin d'être une sinécure. Il sera enfin question d'une conjecture personnelle récalcitrante : cette famille de fonctions semble croissante point-à-point.

NB: Il y aura un recouvrement certain mais loin d'être total avec un exposé précédent aux journées PPS 2018, consacré à l'époque à G et à un exercice au lecteur posé par Hostadter à propos de “l'arbre miroir” de G. Pas besoin ici d'avoir vu cet exposé 2018 !

We present Flèche, an engine for the incremental validation and edition of scientific formalized documents.

Flèche provides a formal document model, based on a notion of functional interpretation for a family of languages plus algebraic effects capturing document dynamics.

Flèche targets existing systems with non-trivial interfaces and documents in their daily use.

Some features of Flèche are: a) hybrid formal documents, where natural language is intermixed with its formal counterpart; b) modular error recovery and handling of incomplete documents; c) incremental, full-project model; d) standard document edition workflow.

We have released a Flèche implementation for the Coq Proof Assistant, `coq-lsp`, that uses the Language Server Protocol (LSP) as an editor API. Together with LSP-capable editors like Visual Studio Code, `coq-lsp` provides a new user interface for the Coq system with unique characteristics.

In this joint talk we will explore proof-theoretic methods to prove Craig and uniform interpolation in modal logics. Iris will start with an introduction of Craig and uniform interpolation in modal logics. Ian will continue with the presentation of existing proofs of Craig and uniform interpolation via sequent calculi for the modal logic K, as well as their mechanisation in Coq. While they are accessible, the understanding of these proofs will allow us to expand on the topic of Bílková’s pen-and-paper proof of uniform interpolation, which has been resisting mechanisation this far. The issues on the porting of the proof for K to GL will be explained. Finally, Iris will discuss the difficulties of adopting the sequent-style proof of uniform interpolation to hypersequent-style calculi. We will discuss joint work with Raheleh Jalali and Roman Kuznets in which uniform interpolation is proved for extensions of modal logic K5 via hypersequent-like calculi.

A computer system is safety-critical when it can cause serious damage to property, the environment, human life, or to society as a whole. Real-world safety-critical systems are also necessarily complex, because, to take into account the interactions between software, hardware, the physical environment, and sometimes their distributed nature (systems of systems), they need to implement a variety of safety measures, in software, hardware, in the system design, at development time, at compile time, and at run-time. Those safety measures which vary from one safety-critical system to another very often lead to a decrease in performance, for a increase in the execution time of software.

This research work is situated in the context of one such system, the communication-based train control (CBTC) system of Siemens Mobility France which operates a number of driverless subway systems around the World, including Paris lines 1, 4, and 14. That system is certified according to the industrial norm EN-50128 and up to the highest Safety Integrity Level 4, required for safety-critical systems with potentially catastrophic consequences. In this context, the thesis looks for an answer to the question of how to automatically optimize the execution time performance of such systems without losing the previously obtained safety guarantees.

The answer provided is provably correct optimization of source code. A first contribution is a source-to-source compiler for VCP Ada (a subset of Ada) programs, that optimizes source code while preserving the formal semantics of the programs. The compiler has been proven correct in the Coq proof assistant and guarantees the equivalence of execution between the original and the optimized program. The compiler copes with the complexities of the platform, due to hardware safety measures, which is important, since real-world safety-critical systems are often susceptible to having such measures, potentially conflicting with existing formally proven optimizing compilers. Moreover, choosing the approach of a source-to-source compilation shows to have methodological advantages over an approach to proven optimizations having a number of intermediate languages, allowing to simplify and diminishing the needed proof effort.

A second contribution is to the problem of provably correct lexical analysis of compilers, which has previously not received a lot of research attention, a weak link in any compilation chain using a proven or qualified compiler. We develop CoqLex, the first Coq-formalized lexer generator, based on a modification of an existing Coq implementation of regular expression matching via Brzozowski derivatives.

The developed theory and tools have been applied to optimize real-world VCP Ada programs of CBTC systems, consisting of thousands of source files, with promising results.

In this talk, I will give an overview of the work I have been doing for my thesis in the past three years, which is an exploration in the design and implementation of graphical interfaces for constructing formal proofs interactively. A guiding principle throughout my thesis is the use of proof theory, which both inspired new ways of representing and interacting with logical entities, and provided solid foundations to certify the design decisions made along the way. In particular, I applied a new methodology in proof theory called “deep inference”, which enables reasoning deep inside arbitrary logical contexts.

In the first part of the talk, I will present our so-called proof-by-action paradigm, where the user builds proofs by executing gestural actions directly on the proof state. Typically, this corresponds to the possibility of clicking, dragging and dropping items which represent the conclusion and hypotheses of the current goal. This will be illustrated through a demonstration of Actema, a prototype of graphical interface implementing these ideas in the setting of intuitionistic first-order logic. The main feature of Actema is its drag-and-drop proof tactic, which can be seen as a powerful generalization of the standard “apply” and “rewrite” tactics found in most proof assistants. I will discuss its proof-theoretical foundation, a technique called “subformula linking”, as well as how we were able to make it available in the Coq proof assistant by building the coq-actema plugin.

In the second part of the talk, I will present a more experimental line of research where I aim to get rid of the traditional symbolic formulas of logic, in favor of a more structured and iconic representation of the proof state. By “iconic”, I mean that the visual representation of logical statements should hint at their meaning, and provide affordances to the ways in which they can be manipulated. It turns out that this has already been investigated by the visionary logician C. S. Peirce at the end of the 19th century, who devised arguably the first diagrammatic proof calculus in history: the existential graphs. I will present my own take on the existential graphs, which has crystallized into a proof system I call the “flower calculus”. With only 7 rules of (deep) inference, the flower calculus is sound and complete for intuitionistic first-order logic. I will conclude with a demonstration of the Flower Prover, another prototype of GUI for theorem proving in the proof-by-action paradigm, whose actions map directly to the rules of the flower calculus.

Constructive foundations have for decades been built upon realizability models for higher-order logic and type theory. Nonetheless, the existing literature on realizability models has several limitations, including the following: 1) first of all, the question “What is a realizability model?” does not have a very satisfying formal answer 2) traditional realizability models have a rather limited notion of computation, which only supports non-termination and avoids many other commonly used effects. Work to address these limitations has typically overlaid structure on top of existing models, such as by using powersets to represent non-determinism, but kept the realizers themselves deterministic. 3) The algebraic structure of existing realizability models taking into account effects in a more direct fashion (as is done in Krivine realizability for instance) is hard to analyze.

In this work, we (Liron Cohen, Ross Tate & myself) alternatively address these limitations by introducing evidenced frames: a general-purpose framework for building realizability models that support diverse effectful computations. We demonstrate that they define a very flexible notion of realizability models, allowing in particular models wherein the realizers themselves can be effectful, such as λ-terms that can manipulate state, reduce non-deterministically, or fail entirely. Beyond the broader notions of computation, we demonstrate that evidenced frames form a unifying framework for (realizability) models of higher-order dependent predicate logic. In particular, we prove that evidenced frames are complete with respect to these models, and that the existing completeness construction for implicative algebras—another foundational framework for realizability—factors through our simpler construction. As such, we conclude that evidenced frames offer an ideal domain for unifying and broadening realizability models.

Most of our results have been formalised in the Coq proof assistant, and I plan to devote some part of the talk to present this formalisation.

Automated tactics in Coq are numerous but often limited to some specific logical fragment. Pre-processing can help them to be efficient in more situations, but it is often specialized to one tactic. This is why we implemented Sniper, a general pre-processing tool made of predictable atomic compositional transformations. Sniper also provides a push-button automated tactic called snipe, which composes the transformations and calls external SMT-solvers within Coq thanks to the SMTCoq plugin.

The traditional big-step semantics judgment relates an input configuration to one output configuration. For a non-deterministic semantics, the big-step judgment does not naturally capture the property that all possible executions are well-behaved. In contrast, the omni-big-step semantics relates an input configuration to a set of reachable output configurations (technically, an overapproximation of that set), and directly captures total correctness properties. I will present the omni-big-step semantics judgment, which corresponds to an inductive definition of a weakest-precondition predicate. I will explain how this judgment leads to the simplest known soundness proof for a sequential Separation Logic, moreover capturing total correctness.

Besides, I will present “characteristic formulae in weakest-precondition style”. These formulae also correspond to the weakest precondition of a unannotated program, that is, a program without specifications nor invariants. Characteristic formulae provide a practical way of embedding Separation Logic reasoning in a proof assistant such as Coq. This approach is implemented in my program verification tool CFML, and is described in an all-in-Coq course, Volume 6 of the Software Foundations series.

Furthermore, I will advertise for two cousins of the omni-big-step semantics: the coinductive-omni-big-step semantics, which captures partial correctness; and the omni-small-step semantics, which relates one configuration to its set of successor configurations. I will explain how omni-semantics may be used to: (1) carry out type-soundness proofs in a style that avoids quadratic case inspections, and (2) carry out compiler correctness proofs using forward simulation proofs, even in the case of nondeterministic semantics.

We discuss the formalization of Linear Logic, through the development of the Yalla library for Coq:

https://perso.ens-lyon.fr/olivier.laurent/yalla/

The initial specification was to get a library which:

• would provide standard results on the proof theory of Linear Logic;
• could be reused, thus in particular able to deal with some variants of the system;
• should be compatible with the Curry-Howard interpretation of proofs, thus faithful to their computational content.

We will describe the evolution of the project and how it matches this specification through the different versions of the library: Yalla 1, Yalla 2 (current version), Yalla 3 (future directions).

Following all previous known works, Yalla 1 defined proofs in Prop. It relies on an explicit exchange rule for dealing with the computational content of proofs. Yalla 2 corresponds to a move to Type to be able to extract computational informations from proofs. Yalla 3 will rely on a different way of approaching exchange to be able to deal with local transformations of proofs more easily.

Le dernier théorème de Fermat est un résultat en théorie des nombres qui a été conjecturé en 1637, mais qui a été démontré seulement en 1995. La démonstration repose sur des techniques mathématiques modernes et sa formalisation est actuellement hors de portée. Dans cet exposé je vais expliquer la formalisation en Lean d'un cas particulier de ce théorème, où l'on suppose que l'exposant est un nombre premier “régulier” (cette notion sera introduite pendant l'exposé). Je vais aussi décrire l'assistant de preuve Lean et sa bibliothèque mathématique mathlib, et j'expliquerai l'intérêt mathématique d'un tel projet. Aucune connaissance en théorie de nombres est nécessaire pour suivre l'exposé.