Groupe de travail

Équipe thématique Preuves et programmes

Jour, heure et lieu

Le mercredi à 14h, salle 1007


Pour recevoir les annonces, s'abonner ici.

Prochaines séances

Séances précédentes

Théorie des types et réalisabilité
lundi 19 mars 2018, 13h15, 3052
Adrien Guatto () A Generalized Modality for Recursion

Nakano’s later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infnite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale.

Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limitations stem from the fact that the later modality is not expressive enough to capture precise input-output dependencies of functions. As a consequence, guarded type theories reject many productive definitions. Combining insights from guarded type theories and synchronous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behaved reindexing of the time scale to a type. We call such reindexings time warps. Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ours.

We integrate our modality into a typed λ-calculus. We equip this calculus with an operational semantics, as well as an adequate denotational semantics in the topos of trees, a standard categorical model for guarded recursion. Building on top of categorical ideas, we describe an abstract type-checking algorithm whose completeness entails the coherence of both semantics.

Théorie des types et réalisabilité
mercredi 14 mars 2018, 14h00, Salle 1007
Laura Fontanella (Institut de Mathématiques de Marseille) L'Axiome du Choix dans la réalisabilité classique

La réalisabilité fournit une interpretation des formules d'un système logique (ou d'une théorie) dans un modèle de calcul. Introduite par Kleene dans les années `40, la réalisabilité est née comme une interprétation des formules de l'arithmétique de Heyting par des ensembles d'indices de fonctions récursives. Avec J.-L. Krivine, la recherche en réalisabilité a évolué jusqu’à englober les axiomes de la théorie des ensembles. Les techniques développées par Krivine fournissent une méthode pour construire des modèles de la théorie des ensembles où tout énoncé de la théorie ZF plus l'Axiome du Choix Dépendant est réalisé. L'Axiome du Choix Dépendant, DC, est une version faible de l'Axiome du Choix; si et comment il serait possible de réaliser l'Axiome du Choix dans sa totalité reste une question ouverte. Nous allons considérer des principes intermédiaires: (1) le principe de partition, PP : étant donné deux ensembles A et B, s’il y a une surjection de A dans B, alors il y a une injection de B dans A; (2) le “Dual Cantor Bernstein theorem”, CB* : s’il y a une surjection de A dans B et une surjection de B dans A, alors A et B sont équipotents; (3) le principe de partition faible, WPP : s’il y a une surjection de A dans B et une injection de A dans B, alors A et B sont équipotents. Ces principes découlent de l'Axiome du Choix et sont plus forts que l'Axiome du Choix Dépendant. Cependant, on ne sait pas s'ils sont équivalents à l'Axiome du Choix et cela est un vieux problème ouvert formulé par B. Banacschewski et G. Moore en 1990. Est-il possible de construire un modèle de réalisabilité pour l'un de ces principes? Cette recherche peut aboutir à deux situations divergentes: soit on trouvera des modèles de réalisabilité pour ces principes où l’axiome du choix est également réalisé, soit on s’arrêtera à une étape donnée sur des modèles de réalisabilité où l’un de ces principes (ou tous) est réalisé, tandis que l’Axiome du Choix ne l’est pas, dans ce dernier cas on aurait alors montré que ces principes ne sont pas équivalents à l’Axiome du Choix et on aurait ainsi résolu le problème de Banacschewski-Moore. Je vous presenterai l'avancement de mes recherches dans ce domaine.

Théorie des types et réalisabilité
mercredi 14 février 2018, 14h00, Salle 1007
Jérôme Siméon (Clause, Inc.) Specifying and compiling domain specific languages using Coq: Three case studies

Domain specific languages (DSL) can be well suited for certain business scenarios and be easier to learn for non-developers. We present our experience using the Coq proof assistant to support the formal specification and the compilation for three different DSLs: JRules (a language for business rules), SQL (a language for relational databases), and Jura (a language for legal contract).

We describe how each of those languages comes with its own challenges, and how they benefit differently from the use of a proof assistant. We also show how we could exploit their commonalities to build an optimizing and (partially) verified compiler for each of them. The core of that compiler uses traditional database representations (the Nested Relational Algebra and its corresponding Calculus) for optimization and code-generation.

– Some of this work was done jointly with Joshua Auerbach, Martin Hirzel, Louis Mandel and Avi Shinnar as part of the Q*cert project (

Théorie des types et réalisabilité
mercredi 31 janvier 2018, 14h00, Salle 1007
Armaël Guéneau (Inria Paris) A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification

I will present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. The framework is built on top of Separation Logic with Time Credits, embedded in the Coq proof assistant. I will formalize the O notation, which is key to enabling modular specifications and proofs, and cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. I will propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.

Théorie des types et réalisabilité
mercredi 17 janvier 2018, 14h00, Salle 1007
Rodolphe Lepigre () Practical Curry-Style using Choice Operators, Local Subtyping and Circular proofs

In a recent (submitted) work with Christophe Raffalli, we designed a rich type system for an extension of System F with subtyping. It includes primitive sums and products, existential types, (co-)inductive (sized) types, and it supports general recursion with termination checking. Despite its Curry-style nature, the system can be (and has been) implemented thanks to new techniques based on choice operators, local subtyping and circular proofs. During the talk, I will give you a flavour of these three ideas. In particular, I will show how choice operators can be used to get rid of free variables (and thus typing contexts), while yielding a clear semantics. I will show how local subtyping can be used to make the system syntax-directed. And I will show how circular proofs may be used to handle (co-)inductive types and (terminating) recursion.

References and links: - paper: - implementation of the system: - online interpreter and examples:

Théorie des types et réalisabilité
mercredi 20 décembre 2017, 14h00, Salle 1007
Ludovic Patey (ICJ, Lyon) Introduction aux mathématiques à rebours

Les mathématiques à rebours sont un domaine fondationnel qui vise à trouver les axiomes optimaux pour prouver les théorèmes de la vie de tous les jours. Elles se placent dans l'arithmétique du second ordre, avec une théorie de base, RCA, capturant informellement les “mathématiques calculables”. Nous reviendrons sur les justifications historiques des mathématiques à rebours, présenterons ses principales observations, ainsi que l'approche moderne des mathématiques à rebours comme formalisme de classification de phénomènes calculatoires.

Théorie des types et réalisabilité
mercredi 06 décembre 2017, 14h00, Salle 1007
Francesco A. Genco (IRIF - TU Wien) Typing Parallelism and communication through hypersequents

We present a Curry–Howard correspondence for Gödel logic based on a simple natural deduction reformulating the hypersequent calculus for this logic. The resulting system extends simply typed λ-calculus by a symmetric higher-order communication mechanism between parallel processes. We discuss a normalisation procedure and several features of the parallel λ-calculus. Following A. Avron's 1991 thesis on the connection between hypersequents and parallelism, we also discuss the generalisation of the employed techniques for other intermediate logics.

Théorie des types et réalisabilité
mercredi 29 novembre 2017, 14h00, Salle 1007
Guilhem Jaber (ENS Lyon) A Trace Semantics for System F Parametric Polymorphism

In this talk, we present a trace model for System F that captures Strachey parametric polymorphism. The model is built using operational nominal game semantics and enforces parametricity by using names. This model is used here to prove a conjecture of Abadi, Cardelli, Curien and Plotkin which states that Strachey equivalence implies Reynolds equivalence (i.e. relational parametricity) in System F.

Théorie des types et réalisabilité
jeudi 16 mars 2017, 14h00, Salle 1007
Pierre-Marie Pédrot () An Effectful Way to Eliminate Addiction to Dependence

We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory, such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin.