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é.