## Séminaire Formath (Formalized Mathematics)

#### Jour, heure et lieu

Le lundi à 14h, 1007 ou 3052

Le calendrier des séances (format iCal).

Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.

#### Contact(s)

Le séminaire Formath (Formalized mathematics) est le séminaire de l'équipe Picube.

Pour s'abonner à la liste de diffusion, consulter la page https://listes.irif.fr/sympa/info/formath ou écrire aux responsables du séminaire.

### Séances passées

#### Année 2023

Formath

Mardi 12 septembre 2023, 10 heures 15, Salle 146, Bâtiment Olympe de Gouges

**Ian Shillito And Iris Van Der Giessen** *Interpolation(s) via proof theory: sequents, Coq, and beyond sequents.*

This will be a joint talk of a duration of about 1H45. Il s'agira d'un exposé commun, d'une durée d'environ 1H45

Formath

Lundi 5 juin 2023, 14 heures, 146 (Olympe de Gouges)

**Wendlasida Ouedraogo** (INRIA (Paris Saclay)) *Source code optimization for safety critical systems*

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.

Formath

Lundi 22 mai 2023, 14 heures, Olympe de Gouges, 146

**Pablo Donato** (Partout Team, LIX laboratory) *Deep Inference for Graphical Theorem Proving*

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.

Formath

Lundi 15 mai 2023, 14 heures, Salle 146, Bâtiment Olympe de Gouges

**Etienne Miquey** (I2M) *Evidenced frames: a unifying framework broadening realizability models (and that is formalised in Coq!)*

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.

Formath

Mardi 9 mai 2023, 11 heures, 147 (Olympe de Gouges)

**Louise Dubois De Prisque** (LSV, CNRS & ENS Paris-Saclay) *Compositional pre-processing for Coq’s tactics*

Formath

Lundi 17 avril 2023, 14 heures, Olympe de Gouges (room 146)

**Arthur Charguéraud** (Camus team, ICPS, iCube, INRIA) *A Modern Eye on Weakest Preconditions*

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.

Formath

Lundi 3 avril 2023, 14 heures, 1007

**Olivier Laurent** (Équipe Plume, Laboratoire de l'Informatique du Parallélisme (LIP), ENS Lyon) *1, 2, 3, Yalla: Linear Logic in 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.

Formath

Lundi 20 mars 2023, 15 heures, 1007

**Riccardo Brasca** (IMJ-PRG, Université Paris-Cité) *Le dernier théorème de Fermat pour les premiers réguliers en Lean*