Équipe-projet Inria $\pi r^2$ (Inria)

Équipe thématique Algèbre et calcul

Équipe thématique Analyse et conception de systèmes

Équipe thématique Preuves et programmes

## Preuves, programmes et systèmes

#### Jour, heure et lieu

Le jeudi à 10h30, en ligne

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)

Pour recevoir les annonces du séminaire PPS, envoyer un courriel à sympa@listes.irif.fr avec comme titre “subscribe seminaire-pps VotrePrénom VotreNom” et un corps vide.

Les membres de PPS peuvent proposer des orateurs et/ou sujets sur l'intranet.

### Prochaines séances

Preuves, programmes et systèmes

Jeudi 8 décembre 2022, 10 heures 30, Salle 3052 & online ([Zoom link|https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09)

**Beniamino Accattoli** (INRIA Saclay, PARTOUT Project-Team) *Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic.*

Preuves, programmes et systèmes

Jeudi 15 décembre 2022, 10 heures 30, Salle 3052

**Davide Barbarossa** (Università di Bologna) *Non encore annoncé.*

Preuves, programmes et systèmes

Jeudi 12 janvier 2023, 10 heures 30, Salle 3052 & online ([Zoom link|https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09)

**Rémy Cerda** (Université d'Aix-Marseille) *Taylor expansion for the infinitary λ-calculus*

Corresponding paper (submitted to LMCS): https://arxiv.org/abs/2211.05608. This is joint work with my supervisor Lionel Vaux Auclair (I2M, AMU).

### Séances passées

#### Année 2022

Preuves, programmes et systèmes

Jeudi 1 décembre 2022, 10 heures 30, Salle 3052 & online (Zoom link)

**David Baelde** (ENS Rennes) *Logical foundations of the Squirrel prover*

Preuves, programmes et systèmes

Jeudi 10 novembre 2022, 10 heures 30, Salle 3052

**Gabriele Vanoni** (Inria Sophia Antipolis) *Reasonable Space and the Lambda-Calculus*

Preuves, programmes et systèmes

Jeudi 13 octobre 2022, 10 heures 30, Salle 3052 & online (Zoom link)

**Willem Heijltjes** (University of Bath) *The Functional Machine Calculus*

Preuves, programmes et systèmes

Jeudi 6 octobre 2022, 10 heures, Salle 3052

**All Hands On Deck** (IRIF) *Matinée de rentrée de PPS*

Preuves, programmes et systèmes

Jeudi 22 septembre 2022, 10 heures 30, ENS Lyon

**Romain Couillet, Claudia Faggian, Guillaume Geoffroy** *Séminaire CHOCOLA*

http://chocola.ens-lyon.fr/events/

Preuves, programmes et systèmes

Lundi 19 septembre 2022, 11 heures, 3052 and Zoom link

**Shachar Itzhaky** (Technion, Haifa) *TheSy: Theory Exploration Powered by Deductive Synthesis and E-graphs*

In this talk, I will present results published in CAV 2021, and ongoing work on extending TheSy to richer theories. In the first work, we used e-graphs on top of egg (Willsey et al). In the follow-up, we extend egg to be able to handle conditional equalities, which are pervasive in many theories; notably, Separation Logic with inductive definitions. We hope that this will allow synthesizing a richer set of lemmas.

Joint session with the Verification seminar.

Preuves, programmes et systèmes

Mercredi 13 juillet 2022, 14 heures 30, Salle 3052

**Daniela Petrisan, Alexandre Goy, Nicolas Munnich, Chris Barrett, Willem Heijltjes And Other Mfps Speakers** *MFPS local event - day 3*

See https://www.cs.cornell.edu/mfps-2022/paris.md.html for additional information.

Preuves, programmes et systèmes

Mardi 12 juillet 2022, 14 heures 30, Salle 3052

**Nicolas Wu And Other Mfps Speakers** *MFPS local event - day 2*

See https://www.cs.cornell.edu/mfps-2022/paris.md.html for additional information.

Preuves, programmes et systèmes

Lundi 11 juillet 2022, 14 heures 30, Salle 3052

**Barbara König, Ayberk Tosun, Frank Pfenning And Other Mfps Speakers** *MFPS local event - day 1*

See https://www.cs.cornell.edu/mfps-2022/paris.md.html for additional information.

Preuves, programmes et systèmes

Jeudi 23 juin 2022, 10 heures 30, Salle 3052 & online

**Lison Blondeau-Patissier** (Aix-Marseille Université) *Positional Injectivity for Innocent Strategies*

This talk is based on a article written with Pierre Clairambault (https://drops.dagstuhl.de/opus/volltexte/2021/14255).

Preuves, programmes et systèmes

Jeudi 16 juin 2022, 10 heures 30, Salle 3052 & online (Zoom link)

**Nicola Gambino** (University of Leeds) *Kripke-Joyal semantics for type theory*

Preuves, programmes et systèmes

Jeudi 9 juin 2022, 10 heures 30, Salle 3052

**Jonathan Sterling** (University of Aarhus) *Naïve logical relations in synthetic Tait computability*

Preuves, programmes et systèmes

Jeudi 2 juin 2022, 10 heures 30, Online (Zoom link)

**Cezary Kaliszyk** (University of Innsbruck) *Property Invariant Machine Learning for Theorem Proving*

Preuves, programmes et systèmes

Jeudi 19 mai 2022, 10 heures 30, On-line.

**Glynn Winskel** (Huawei Edinburgh Research Centre) *Making Concurrency Functional*

- several paradigms of functional programming and logic arise naturally as subcategories of concurrent games, including stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation; lenses and optics; and their extensions to containers in dependent lenses and optics.

- to transfer enrichments of strategies (such as to probabilistic, quantum or real-number computation) to functional settings.

Preuves, programmes et systèmes

Jeudi 12 mai 2022, 10 heures 30, Salle 3052

**Patrick Baillot** (CNRS, CRIStAL Lille) *Bunched Fuzz: Sensitivity for Vector Metrics*

This is joint work with june wunder, Arthur Azevedo de Amorim, and Marco Gaboardi.

Preuves, programmes et systèmes

Jeudi 5 mai 2022, 10 heures 30, Salle 3052

**Marcelo Fiore** (University of Cambridge) *The Mathematical Foundations of a Formal Computational Metatheory of Second-Order Algebraic Theories*

Specifically, I will present a new categorical model for Second-Order Algebraic Theories: it is based on indexed families and founded upon the initial-algebra approach. A main motivation for and crucial aspect of the mathematical theory is that it is directly programmable in languages supporting inductive families; and, indeed, was developed in unison with building a formally-verified computer implementation for second-order semantics, computation, and deduction. As such, the work resulted in a framework within the Agda proof assistant for the automatic generation of generic second-order abstract syntax and provably-correct metaoperations for manipulating it; to wit, algebraic models together with compositional interpretations, capture-avoiding and metavariable substitution operations, and equational and/or rewriting reasoning. This is joint work with Dmitrij Szamozvancev; a paper, source code, documentation, and case studies are available at the project page <tinyurl.com/agda-soas>.

Preuves, programmes et systèmes

Jeudi 28 avril 2022, 10 heures 30, Salle 3052

**Antonino Salibra** (IRIF & Università Ca'Foscari) *Universal clone algebra*

Preuves, programmes et systèmes

Jeudi 21 avril 2022, 10 heures 30, Salle 3052

**Laura Fontanella** (Université Paris-Est Créteil) *Representing ordinals in classical realizability*

Preuves, programmes et systèmes

Jeudi 7 avril 2022, 10 heures 30, Salle 3052 & online

**Pierre Clairambault** (CNRS, Aix-Marseille Université) *The Geometry of Causality : Multi-Token Geometry of Interaction and its Causal Unfolding*

To prove our machine correct, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. We define Petri strategies as those Petri structures obeying the rules of the game. In turn, we show how Petri strategies unfold to concurrent strategies in the sense of concurrent games on event structures. This not only entails correctness and adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types.

This is joint work with Simon Castellan. The Geometry of Causality machine is implemented, and available at: https://ipatopetrinets.github.io/

Preuves, programmes et systèmes

Jeudi 31 mars 2022, 10 heures 30, Online

**Cristina Matache, Abhishek De, Federico Olimpieri** *Séminaire CHOCOLA*

Preuves, programmes et systèmes

Jeudi 24 mars 2022, 10 heures 30, Online

**Matteo Acclavio** (Université du Luxembourg) *Designing graphical proof systems*

Online at link (any password works)

Preuves, programmes et systèmes

Jeudi 17 mars 2022, 10 heures 30, Salle 3052 & online

**Gabriel Scherer** (Inria Saclay) *A right-to-left type system for recursive value definitions*

Our analysis is described by a set of declarative inference rules that can be “directed” into an algorithmic check. Our implementation of this check replaced the existing check used by the OCaml programming language, a fragile syntactic/grammatical criterion which let several subtle bugs slip through as the language kept evolving.

https://galene.org:8443/group/seminaire-pps (any password works)

Preuves, programmes et systèmes

Jeudi 10 mars 2022, 10 heures 15, On-line.

**Tba** *Séminaire CHOCOLA*

Preuves, programmes et systèmes

Jeudi 3 mars 2022, 10 heures 30, Salle 3052 and virtual room at link (any password works)

**Mirna Džamonja** (IRIF) *Soundness after Gödel*

On suivra la tradition où les transparents sont en anglais et la langue de présentation le français si tout le monde est francophone, l’anglais autrement.

Preuves, programmes et systèmes

Jeudi 17 février 2022, 10 heures 30, Room 3052 and virtual room at link (any password works)

**Xavier Denis** (LMF, Paris-Saclay) *Creusot: A prophetic verifier for Rust*

We present Creusot, a tool for the formal specification and deductive verification of Rust. Creusot's specification language features a notion of prophecies to reason about memory mutation. Rust provides advanced abstraction features based on a notion of traits, extensively used in the standard library and in user code. The support for traits is at the heart of Creusot's approach of verification and specification of programs.

Preuves, programmes et systèmes

Jeudi 27 janvier 2022, 10 heures 30, Room 3052 and virtual room at link (any password works)

**Titouan Carette** (LORIA / Université de Lorraine) *Diagrammatic semantics of quantum streams*

Preuves, programmes et systèmes

Jeudi 20 janvier 2022, 10 heures 15, Virtual room at link

**Bruno Dinis** (Universidade de Lisboa) *Functional interpretations and applications*

I will present several recent functional interpretations and some results that come from these interpretations. I will also give examples of application of functional interpretations, in the spirit of the proof mining program.

Séminaire CHOCOLAT.

Preuves, programmes et systèmes

Jeudi 13 janvier 2022, 10 heures 30, Virtual room at link (any password works)

**Xavier Rival** (École normale supérieure) *Towards Verified Stochastic Variational Inference for Probabilistic Programs*

In this talk, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs' denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural network models such as AIR. It finds a bug in one of these cases, reveals a non-standard use of an inference engine in another, and shows that the assumptions are met in the remaining six cases.

(Joint work with Wonyeol Lee, Hangyeol Yu, and Hongseok Yang, KAIST)

#### Année 2021

Preuves, programmes et systèmes

Jeudi 16 décembre 2021, 10 heures 30, Virtual room at link (any password works)

**Vasileios Koutavas** (Trinity College Dublin) *From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques*

In this talk we present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract symbolic environmental bisimulations similar to symbolic game semantics, up-to techniques, and lightweight state invariant annotations. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We have realised the technique in a tool prototype called Hobbit and benchmarked it with an extensive set of new and existing examples. Hobbit can prove many classical equivalences including all Meyer and Sieber examples.

Preuves, programmes et systèmes

Vendredi 10 décembre 2021, 10 heures 30, Virtual room at link (any password works)

**Jérémy Ledent** (University of Strathclyde) *Simplicial Models for Multi-Agent Epistemic Logic*

This is joint work with Éric Goubault and Sergio Rajsbaum

Preuves, programmes et systèmes

Jeudi 2 décembre 2021, 10 heures 30, Virtual room at link (any password works)

**Sylvain Boulmé** (Verimag) *Formally Verified Assembly Optimizations by Symbolic Execution.*

With Cyril Six and David Monniaux, we solved this performance issue with formally verified hash-consing within the symbolic execution. And we successfully applied this technique to implement within CompCert effective optimizations targeting superscalar (or VLIW) in-order processors.

The talk will actually start by briefly introducing a sound Foreign Function Interface for embedding OCaml oracles within Coq. Hence, it will explain how we used it in this application.

This talk will be in French.

Preuves, programmes et systèmes

Jeudi 25 novembre 2021, 10 heures 30, Room 3052 and virtual room at link (any password works)

**Denis Merigoux** (INRIA) *Catala: A Programming Language for the Law*

Preuves, programmes et systèmes

Jeudi 18 novembre 2021, 10 heures 30, Room 3052 and virtual room at link (any password works)

**Aymeric Fromherz** (INRIA) *Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic*

In this talk, we give an overview of Steel from the ground up. To reason about programs, Steel provides a higher-order, impredicative concurrent separation logic with support for dynamically-allocated invariants and partial commutative monoids (PCMs). To automate verification, Steel separates verification conditions between separation logic predicates and first-order logic encodeable predicates; we develop a (partial) decision procedure using efficient, reflective tactics that focuses on the former, while the latter can be encoded efficiently to SMT by F*. We will conclude by presenting several verified Steel libraries, including mutable, self-balancing trees as well as a novel PCM-based encoding of 2-party dependently typed sessions, that illustrate the expressiveness and programmability of Steel.

This talk will be in English.

Preuves, programmes et systèmes

Jeudi 21 octobre 2021, 10 heures 15, On-line.

**Armaël Guéneau** (Aarhus) *Program verification on a capability machine in the presence of untrusted code*

This talk is joint with the CHOCOLA seminar. See https://chocola.ens-lyon.fr/events/online-2021-10-22/ for details.

Preuves, programmes et systèmes

Jeudi 1 juillet 2021, 10 heures, Online

**Daniele Varacca** *Milner and Alur walk into a bar*

This talk will start from Morris' PhD thesis in 1968 and present 50 years of theoretical computer science, through PCF, CCS, Alternating transition systems, contexts and strategies, ending up at the footsteps of the monumental Palace of Justice in Créteil.

This talk is joint with the CHOCOLA seminar. See https://chocola.ens-lyon.fr/events/online-2021-07-01/talks/varacca/ for details.

Preuves, programmes et systèmes

Jeudi 24 juin 2021, 17 heures, Online at link (any password works)

**Michael Shulman** (University of San Diego) *Affine logic for constructive mathematics*

I will show that intuitionistic and linear approaches to constructive mathematics are intimately connected, through an interpretation of linear logic (or more precisely, affine logic) into intuitionistic logic based on a categorical Chu/Dialectica construction called the “antithesis translation”. In particular, many odd features of intuitionistic mathematics, such as inequality relations, anti-subgroups, and apartness spaces, arise automatically and unavoidably by translating natural definitions from affine logic across this interpretation. Thus, affine logic can be used as a “high-level tool” for intuitionistic mathematics, helping to find the right definitions and manage the bookkeeping of formally dual properties in proofs.

Preuves, programmes et systèmes

Jeudi 17 juin 2021, 10 heures, Online

**Sonia Marin** *Focused nested calculi applied to the logic of bunched implications*

With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied, following the method introduced by O. Laurent, on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed by a polarised and focused variant that (again) we show is sound and complete via a cut-elimination argument.

This talk is joint with the CHOCOLA seminar. See https://chocola.ens-lyon.fr/events/online-2021-06-17/talks/marin/ for details.

Preuves, programmes et systèmes

Jeudi 10 juin 2021, 10 heures 30, Online at link (any password works)

**Paul-André Melliès** (IRIF) *A gentle introduction to template games*

The interested reader will find more material here https://www.irif.fr/~mellies/template-games.html https://www.youtube.com/watch?v=ZC2jtq2R3cw and in the companion papers [1,2,3].

[1] PAM. Categorical combinatorics of scheduling and synchronization in game semantics. Proceedings of POPL 2019. https://www.irif.fr/~mellies/papers/Mellies19popl.pdf https://www.irif.fr/~mellies/slides/popl-slides-january-2019.pdf

[2] PAM. Template games and differential linear logic. Proceedings of LICS 2019. https://www.irif.fr/~mellies/template-games/2-template-games-and-differential-linear-logic.pdf

[3] PAM. Asynchronous template games and the Gray tensor product of 2-categories. Proceedings of LICS 2021. https://www.irif.fr/~mellies/papers/asynchronous-template-games.pdf

[4] PAM. Une étude micrologique de la négation https://www.irif.fr/~mellies/hdr-mellies.pdf

Preuves, programmes et systèmes

Jeudi 3 juin 2021, 15 heures, Online

**Carlo Angiuli** (Carnegie Mellon University) *Internalizing Representation Independence with Univalence*

In this talk, we describe a technique for establishing internal relational representation independence results in Cubical Agda by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at https://dl.acm.org/doi/10.1145/3434293.

This talk is joint with the CHOCOLA seminar. See https://chocola.ens-lyon.fr/events/online-2021-06-03/talks/angiuli/ for details.

Preuves, programmes et systèmes

Jeudi 27 mai 2021, 10 heures 30, Online at link (any password works)

**Xavier Rival** (École normale supérieure) *Non encore annoncé.*

(Joint work with Hugo Illous and Matthieu Lemerre.)

Preuves, programmes et systèmes

Jeudi 20 mai 2021, 10 heures, Online

**Valeria Vignudelli** (École normale supérieure de Lyon) *Monads, equational theories, and metrics for nondeterministic and probabilistic systems*

Bibliography:

Bonchi, Sokolova, Vignudelli. The theory of traces for systems with nondeterminism and probabilities. LICS 2019. Available at: https://arxiv.org/abs/1808.00923

Mio, Vignudelli. Monads and quantitative equational theories for nondeterminism and probabilities. CONCUR 2020. Available at: https://arxiv.org/abs/2005.07509

Mio, Sarkis, Vignudelli. Combining nondeterminism, probability, and termination: equational and metric reasoning. LICS 2021. Available at: https://arxiv.org/abs/2012.00382

This talk is joint with the CHOCOLA seminar. See https://chocola.ens-lyon.fr/events/online-2021-05-20/talks/vignudelli/ for details.

Preuves, programmes et systèmes

Jeudi 6 mai 2021, 10 heures, Online

**Barbara König** *Fixpoint Theory - Upside Down*

The theory is developed for non-expansive monotone functions on suitable lattices of the form M^Y, where Y is a finite set and M an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.

This talk is joint with the CHOCOLA seminar. See https://chocola.ens-lyon.fr/events/online-2021-05-06/talks/konig/ for details.

Preuves, programmes et systèmes

Jeudi 29 avril 2021, 10 heures 30, Online at link (any password works)

**Gabriel Scherer** (Inria Saclay) *Normalization by realizability: a dependently typed pearl*

(If you are unfamiliar with classical realizability, it might help to think of it as a unary logical relation with an elegant symmetric setup – it originates in studies of classical logic. The talk will gently introduce classical realizability.)

Two salient points of our presentation correspond to folklore ideas that we present as opinionated recommandations, to ourselves and others, of how to give a “modern” presentation of these questions (classical realizability, and in general studying the computational content of a proof device):

1. We present classical realizablity as compilation to Curien-Herbelin style symmetric abstract machine calculi, instead of the Krivine Abstract Machine, to represent realizers. Experts will recognize the polarized reduction rules of Munch-Maccagnoni.

2. To present computation content, we are *not* using extraction of a program from a mathematical-style proof in a proof assistant. That beautiful approach rarely works and it generates ugly code. Instead we *write* the logical argument directly as a program in a dependently-typed (meta)language, and we think about the code we are writing.

Preuves, programmes et systèmes

Jeudi 22 avril 2021, 10 heures, Online

**Gabriele Vanoni** (Università di Bologna) *The Time and Space of Interaction*

This talk is joint with the CHOCOLA seminar. See https://chocola.ens-lyon.fr/events/online-2021-04-22/ for details.

Preuves, programmes et systèmes

Jeudi 1 avril 2021, 10 heures 30, https://galene.org:8443/group/seminaire-pps

**Pierre-Evariste Dagand** (LIP6) *A Programming Model for Transiently-Powered Systems*

Preuves, programmes et systèmes

Jeudi 1 avril 2021, 14 heures, https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk

**Pps Members** (IRIF) *Journée PPS*

Preuves, programmes et systèmes

Lundi 29 mars 2021, 14 heures, https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk

**Pps Members** (IRIF) *Journée PPS*

Preuves, programmes et systèmes

Mardi 23 mars 2021, 10 heures 30, https://galene.org:8443/group/seminaire-pps

**C. Keller** (Université Paris-Saclay) *SMTCoq: safe and efficient automation in Coq*

In this talk, I will concisely introduce the communication between Coq and external provers, before presenting the new framework of logical transformations. I will report on work in progress of examples of transformations in this framework.

This is joint work with Valentin Blot, Louise Dubois de Prisque and Pierre Vial.

Preuves, programmes et systèmes

Mardi 23 mars 2021, 14 heures, https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk

**Pps Members** (IRIF) *Journée PPS*

Preuves, programmes et systèmes

Lundi 22 mars 2021, 14 heures, https://galene.org:8443/group/seminaire-pps

**Pps Members** (IRIF) *Journée PPS*

Preuves, programmes et systèmes

Jeudi 4 mars 2021, 10 heures 30, Online

**Micaela Mayero** (Université Sorbonne Paris Nord) *Formalisation en Coq de problèmes numériques: un exemple avec l'intégrale de Lebesgue*

Je présenterai le but à long terme dans lequel s'inscrit ce travail, domaine de la sécurité, de la fiabilité et de la sûreté. Il s'agit de poser les fondements qui nous permettront de prouver la correction d'une bibliothèque implantant la MEF en C++, telle que FELiScE (Finite Elements for Life Sciences and Engineering). Sa vérification formelle augmentera la confiance dans tous les codes qui l'utilisent. Ces travaux sont interdisciplinaires (logique/preuve de programmes/analyse numérique). Ces preuves reposent entre autres sur les bases mathématiques telles que la théorie de la mesure, l'intégrale de Lebesgue, les distributions, les espaces de Sobolev jusqu'à la construction de l'espace fonctionnel L2. Dans cet exposé je m'attarderai sur la formalisation de l'intégrale de Lebesgue pour les fonctions positives.

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 25 février 2021, 10 heures 30, Online

**Adrian Francalanza** (University of Malta) *An Operational Guide to Monitorability*

This is joint work with Luca Aceto, Antonis Achilleos, Anna Ingolfsdottir and Karoliina Lehtinen

Virtual room at link (any password works)

Preuves, programmes et systèmes

Mercredi 24 février 2021, 14 heures, https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7

**Elaine Pimentel** (UFRN - Brazil) *On linear logic, modalities and frameworks*

We then move to the question of giving an interpretation to subexponentials. We will show a game interpretation of affine linear logic with subexponentials, viewing the game as a playground for illuminating semantic intuitions underlying resource conscious reasoning. Interestingly enough, this led to the proposal of new sequent systems for capturing the notions of costs and budget in a fragment of linear logic with subexponentials, thus opening new possibilities for analysing the problem of comparing proofs.

We finish the talk by showing a computational interpretation of subexponentials in the process-as-formula fashion, where process constructors are mapped to logical connectives and computational steps are related to proof steps. In particular, we will show in detail the role of pre-orders in subexponentials for the adequate specification of different modalities in concurrent systems, such as time, space, epistemic and preferences. We end with a discussion about which new models of computation should arise from the extension of the concept of modality in linear logic.

Preuves, programmes et systèmes

Jeudi 18 février 2021, 10 heures 30, Online

**Samuele Giraudo** (Université Gustave Eiffel) *Rewrite systems on free clones and realizations of algebraic structures*

Joint session with the Combinatoire seminar.

Virtual room at link (any password works)

Preuves, programmes et systèmes

Vendredi 12 février 2021, 14 heures, On-line

**Thibaut Benjamin** (LIX) *CaTT : Une theorie des types qui decrit les omega-categories faibles*

Virtual room at link Joint seminar with the GT “Catégories supérieures, polygraphes et homotopie”.

Preuves, programmes et systèmes

Jeudi 11 février 2021, 10 heures 30, Online

**Antoine Genitrini** (LIP6) *The Combinatorics of Barrier Synchronization in Concurrency*

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 4 février 2021, 10 heures 30, Online

**Romain Péchoux** (Université de Lorraine) *Implicit Complexity: to infinity… and beyond!*

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 28 janvier 2021, 10 heures 30, Online

**Jérôme Feret** (INRIA) *Conservative approximation of systems of polymers*

The over-approximation of each derivative relies on symbolic reasoning. We use Kappa to describe our models. Kappa is a site-graph rewriting languages which is popular to describe protein-protein interaction networks. The main ingredients of Kappa, graph patterns, can be interpreted in two ways. Intensionally by the means of embeddings between graphs, or extensionally as the (potentially infinite) multi-sets of the complete graphs they occur in. This second interpretation leads to the definition of positive series of concentration of species. Interestingly, it can be proven that some universal constructions between graphs induce generic methods to prove the well-posedness of some numerical series, and some equality and inequality among them, hence providing a convenient tool-kit for symbolic reasoning

Virtual room at link (any password works)

#### Année 2020

Preuves, programmes et systèmes

Jeudi 17 décembre 2020, 10 heures 30, Online

**Vincent Rahli** (University of Birmingham) *Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle*

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 3 décembre 2020, 10 heures 30, Online

**Laure Gonnord** (Université Lyon Claude Bernard) *Contributions in static analyses for memory: the example of arrays*

In this talk I will present two experiences in the design of static analyses dedicated to array properties and explore the intrinsic difficulties we, together with my coauthors, faced while developing them. I will also show some experimental evidence of the impact of this work on real-world compilers, as well as future perspective for this area of research.

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 26 novembre 2020, 10 heures 30, Online

**Ambroise Lafont** (CSIRO) *Mathematical specifications of programming languages via modules over monads*

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 19 novembre 2020, 10 heures 30, Online

**Benoît Valiron** (CentraleSupelec & LRI) *From symmetric pattern-matching to quantum control*

In this talk, we argue that, under the right circumstances, a reasonable notion of quantum loop is possible. To this aim, we propose a typed, reversible language with lists and fixpoints, extensible to linear combinations of terms. The language admits a reduction strategy in the spirit of algebraic lambda-calculi. Under the restriction of structurally recursive fixpoints, it is shown to capture unitary operations. It is expressive enough to represent several of the unitaries one might be interested in expressing.

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 12 novembre 2020, 10 heures 30, Online

**Marc De Visme** *Game Semantics for Quantum Programming*

Link (any password works)

Preuves, programmes et systèmes

Jeudi 5 novembre 2020, 10 heures 30, Online

**Robin Piedeleu** (University College London) *A diagrammatic axiomatisation of finite-state automata*

Preuves, programmes et systèmes

Jeudi 29 octobre 2020, 15 heures, Online at this link

**Jan Hoffmann** (Carnegie Mellon University) *Raising Expectations: Automating Expected Cost Analysis with Types*

In this talk, I will first give an overview of AARA for deterministic programs and some of the innovations that have been introduced over the past decade. I will then describe our novel results on expected bound analysis for probabilistic programs, highlight the challenges of adopting AARA to a probabilistic language, present experimental results, and discuss some open problems.

Preuves, programmes et systèmes

Jeudi 22 octobre 2020, 10 heures 30, Online at this link

**Sylvain Salvati** (Université de Lille) *Syntactic properties from a semantic perspective*

Preuves, programmes et systèmes

Jeudi 15 octobre 2020, 10 heures, Online

**Nicolas Behr, Camille Combe, Hugo Moeneclaey, Sylvain Douteau** *Journées de rentrée PPS 2020*

Preuves, programmes et systèmes

Jeudi 8 octobre 2020, 10 heures 30, Online

**Vincent Blazy, Zeinab Galal, Farzad Jafar-Rahmani, Ada Vienot** *Journées de rentrée PPS 2020*

- Hugo Herbelin: présentation des axes scientifiques du pôle PPS.

- Vincent Blazy: Structure fine du Sous-Typage d’Univers en CCI et applications à la certification de programmes et aux Fondements des Mathématiques.

- Zeinab Galal: A Profonctorial Finiteness Semantics;

- Farzad Jafar-Rahmani: Denotational semantics of logic with fixed points.

- Ada Vienot: tba

Preuves, programmes et systèmes

Jeudi 1 octobre 2020, 10 heures 30, Online

**Kostia Chardonnet, El-Mehdi Cherradi, Simon Forest, Mickael Laurent** *Journées de rentrée PPS 2020*

- Kostia Chardonnet: Towards a Curry-Howard Correspondence for Quantum Computation

- El-Mehdi Cherradi: Preuves, programmes et homotopie

- Simon Forest: Des constructions génériques pour les catégories supérieures

- Mickael Laurent: Intégration d'outils de programmation avancés dans un langage avec types ensemblistes

Preuves, programmes et systèmes

Jeudi 18 juin 2020, 15 heures 30, Online

**Andrei Paskevich** (Paris Sud University) *Abstraction and Genericity in Why3*

This talk presents the modularity features of WhyML, the language of the program verification tool Why3. Instead of separating abstract interfaces and fully elaborated implementations, WhyML uses a single concept of “module”, a collection of abstract and concrete declarations, and a basic operation of “cloning” which instantiates a module with respect to a given partial substitution, while verifying its soundness. This mechanism brings into WhyML both abstraction and genericity, as illustrated by a small verified Bloom filter implementation, translated into executable idiomatic C code.

Preuves, programmes et systèmes

Jeudi 11 juin 2020, 15 heures 30, Online

**Claude Stolze** *Union, intersection and dependent types in an explicitly typed lambda-calculus*

Preuves, programmes et systèmes

Mercredi 10 juin 2020, 15 heures, Online

**Yannick Zakowski** (University of Penn) *Representing recursive and impure programs in Coq: from a toy assembly language to a modular formal semantics for LLVM IR*

ITrees are expressive enough to serve as a language of specification for many projects of the DeepSpec ecosystem, making them a convenient Franca Lingua for formal specification, and helping in connecting projects together. Furthermore, their ability to be extracted make them compatible with ambitions of liveness and two-sidedness.

In this talk, we will particularly focus on how ITrees can be used in the context of verified compilation. To this end, we will first introduce the core concepts over a toy language, before sketching how we have been scaling the approach to LLVM IR as part of the Vellvm DeepSpec project.

Preuves, programmes et systèmes

Mardi 9 juin 2020, 16 heures, Online

**Paul Brunet** (University College London) *Recent developments in concurrent Kleene algebra*

In this talk, I will start by recalling the basic definitions of CKA, and its decidability and completeness theorems. We will then take an overview of some of its extensions, considering aspects such as control-flow, memory consistency and mutual exclusion.

This talk is the result of collaborations with Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, and Georg Struth.

Preuves, programmes et systèmes

Jeudi 28 mai 2020, 15 heures 30, Online

**Glen Mével** (INRIA Cambium) *Towards a separation logic for Multicore OCaml*

There is now a call for reasoning principles for shared-memory concurrency. In real-world applications, shared memory typically exhibits counter-intuitive behaviors, and “weak” memory models are required to describe them. This poses specific challenges for program verification.

After introducing the weak memory model of Multicore OCaml, I will derive a program logic for this language, and demonstrate its usage on simple examples.

I will show how, in our logic, the invariants of these concurrent data structures extend from the naive model of memory to the weaker model enforced by Multicore OCaml. This model is simpler than that of C11, and we argue that our logic exhibits primitive reasoning principles that are easier to deal with than what was possible for C11.

This work builds on the Iris concurrent separation logic framework and is fully mechanized in Coq.

Preuves, programmes et systèmes

Jeudi 14 mai 2020, 15 heures 30, Online

**Pierre-Yves Strub** (École polytechnique) *Jasmin/EasyCrypt: high-assurance, low-level programming*

In this talk, I will present the Jasmin-EasyCrypt project that explores how formal approaches could eliminate this disconnect and bring together implementations (most importantly, efficient implementations) and software artefacts, in particular machine-checked proofs, supporting security analyses.

Preuves, programmes et systèmes

Jeudi 7 mai 2020, 15 heures 30, Online

**Hugo Herbelin** (IRIF) *Introduction à la théorie des types homotopiques, deuxième partie*

Preuves, programmes et systèmes

Jeudi 30 avril 2020, 15 heures 30, Online

**Hugo Herbelin** *Introduction à la théorie des types homotopiques*

Nous donnerons les principes de base de la manière de pensée « HoTT » : principle d'univalence (= extensionalité des types), inductifs supérieurs (généralisation des pushouts), niveaux d'homotopie (h-niveaux), correspondance entre preuves d'égalité et chemins, correspondance propositions/types/espaces/∞-groupoïdes, description « synthétique » d'espaces géométriques (par exemple, cercle = pure donnée algébrique d'un point et d'un chemin autour de ce point), construction de Grothendieck reliant ΣB.(B→A) et A→Type.

Nous pourrions aussi aborder la théorie des types cubiques vue comme style direct pour la paramétricité itérée délimitée. Nous pourrions aussi essayer d'ébaucher le dictionnaire permettant de connecter les vocabulaires informatique/logique/géométrique/catégorique.

À noter que l'exposé essaiera en premier lieu de répondre à la curiosité de l'auditoire et le plan donné pourra évoluer en fonction des questions posées.

Preuves, programmes et systèmes

Jeudi 9 avril 2020, 15 heures 30, Online

**Charles Grellois** (Université d'Aix-Marseille) *Verification of (probabilistic) functional programs*

Preuves, programmes et systèmes

Jeudi 26 mars 2020, 14 heures, Online

**Sam Van Gool** *Model completeness in logical algebra*

Slightly longer abstract: Logical systems of deduction often resemble algebraic systems of equation resolution. The simplest instance of this resemblance is the fact that classical propositional logic essentially boils down to studying algebras over the two-element field. When one changes the logical deduction system, the algebraic structures become less simple, and more interesting; this is where one enters the world of Heyting algebras, modal algebras, and generalizations of such.

The aim of our work here is to gain a better understanding of such logical-algebraic structures by studying them from the perspective of model theory. In the model-theoretic study of usual algebra, the concept of model completeness plays a central role: it provides the correct abstraction of the concept of an algebraically closed field. We show that model completeness also has an important role to play in logical algebra.

In particular, we will discuss two cases of model completeness: intuitionistic logic, and linear temporal logic. In the former, model completeness can be seen to be closely related to a certain interpolation property of the logic, originally established by Pitts. In the latter, automata on infinite words are the technical ingredient that leads to model completeness.

This seminar will take place online. More information soon!

Preuves, programmes et systèmes

Jeudi 13 février 2020, 10 heures 45, Salle 1007

**Cyrille Chenavier** (Inria Lille) *Topological rewriting systems applied to standard bases and syntactic algebras*

(Attention : le séminaire aura exceptionnellement lieu en **salle 1007**.)

Preuves, programmes et systèmes

Jeudi 23 janvier 2020, 10 heures 30, Salle 3052

**Robert Atkey** (University of Strathclyde) *Resource Constrained Programming with Full Dependent Types*

Preuves, programmes et systèmes

Jeudi 16 janvier 2020, 10 heures 30, Salle 3052

**Gabriel Radanne** (University of Freiburg) *Kindly Bent to Free Us*

While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper resource handling. Linear and affine types guarantee single-threaded resource usage, but they are rarely deployed as they are too restrictive for real-world applications.

We present Affe, an extension of ML with constrained types that manages linearity and affinity properties through kinds. In addition Affe supports the exclusive and unrestricted borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: an impure, strict functional expression language with complete principal type inference and type abstraction through modules. Our language does not require any linearity annotations in expressions and supports common functional programming idioms.

Preuves, programmes et systèmes

Vendredi 10 janvier 2020, 10 heures, Salle 3014

**Joseph Tassarotti** (Boston College) *Verifying Concurrent Randomized Programs*

This talk will describe Polaris, a logic for reasoning about programs that are both concurrent and randomized. Polaris combines ideas from three separate lines of work: (1) Varacca and Winskel's denotational model of non-determinism and probability, (2) Barthe et al.'s approach to probabilistic relational reasoning via couplings, and (3) higher-order concurrent separation logic, as realized in the Iris verification framework.

(Joint session between the PPS and Verification seminars.)

#### Année 2019

Preuves, programmes et systèmes

Jeudi 12 décembre 2019, 10 heures 30, École normale supérieure de Lyon

**Amina Doumane, Cristina Matache** *Séminaire Chocola*

Preuves, programmes et systèmes

Jeudi 28 novembre 2019, 10 heures 30, Salle 3052

**Valeria Vignudelli** (École normale supérieure de Lyon) *Bisimulations and trace equivalences for nondeterministic probabilistic systems*

Preuves, programmes et systèmes

Jeudi 21 novembre 2019, 10 heures 30, Salle 3052

**Giulio Manzonetto** (LIPN and Université Paris Nord) *About the power of Taylor expansion*

A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.

Preuves, programmes et systèmes

Jeudi 14 novembre 2019, 10 heures 30, École normale supérieure de Lyon

**Francesco Gavazzo, Marie Kerjean, Yann Régis-Gianas** *Séminaire Chocola*

Preuves, programmes et systèmes

Jeudi 17 octobre 2019, 10 heures 30, École normale supérieure de Lyon

**Eric Finster** *Séminaire Chocola*

Preuves, programmes et systèmes

Jeudi 3 octobre 2019, 10 heures 30, Salle 3052

**Nicolas Behr** (IRIF) *Stochastic dynamics of graph-like structures*

Preuves, programmes et systèmes

Jeudi 26 septembre 2019, 10 heures 30, École normale supérieure de Lyon

**Pierre Clairambault, Andrea Condoluci, Hugo Férée** *Séminaire Chocola*

Preuves, programmes et systèmes

Lundi 2 septembre 2019, 9 heures 30, Amphithéâtre Turing

**Divers Orateurs** *Journées PPS 2019*

Programme détaillé disponible sur la page https://www.irif.fr/rencontres/pps2019/index.

Preuves, programmes et systèmes

Jeudi 20 juin 2019, 10 heures 30, Salle 3052

**Alex Simpson** (University of Ljubljana) *Sheaf principles for reasoning about probabilistic independence*

Preuves, programmes et systèmes

Mercredi 19 juin 2019, 14 heures 30, Salle 3052

**Ugo Dal Lago** (INRIA and Univ. Bologna) *The Geometry of Bayesian Programming*

Joint work with Naohiko Hoshino

Preuves, programmes et systèmes

Lundi 17 juin 2019, 11 heures, Salle 3052

**Pierre-Malo Deniélou** (Google) *From MapReduce to Apache Beam: A Journey in Abstraction*

Processing large amounts of data used to be an affair of specialists: specialized hardware, specialized software, specialized programming model, specialized engineers. MapReduce was the first widely adopted high-level API for large-scale data processing. It helped democratize big data processing by providing a clear abstraction that was supported by several efficient systems. In this talk, I will present how the programming APIs (and underlying systems) for large-scale data processing evolved in the past 20 years, both within Google and in the open source world. I will start from MapReduce and Millwheel and finish with Apache Beam and where we're headed next.

Preuves, programmes et systèmes

Jeudi 13 juin 2019, 10 heures 30, Salle 3052

**Dan Ghica** (University of Birmingham, UK) *The next 700 abstract machines*

Joint work with Koko Muroya and Todd Waugh Ambridge.

Preuves, programmes et systèmes

Mardi 11 juin 2019, 11 heures, Salle 3052

**Marco Gaboardi** (Buffalo University, USA) *Differential Privacy: Formal Verification and Applications*

Preuves, programmes et systèmes

Jeudi 6 juin 2019, 10 heures 30, Salle 3052

**Jean Goubault-Larrecq** (ENS Cachan) *A Probabilistic and Non-Deterministic Call-by-Push-Value Language*

Preuves, programmes et systèmes

Jeudi 16 mai 2019, 10 heures 30, Salle 3052

**Lionel Vaux** (Amu, Marseille) *An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets*

Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative expo- nential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfies our constraints.

(Joint work with Jules Chouquet.)

Preuves, programmes et systèmes

Jeudi 2 mai 2019, 10 heures 30, Salle 3052

**Hugo Férée** (University of Kent) *Une théorie de la complexité d'ordre supérieur via la sémantique des jeux*

En nous appuyant sur la sémantique des jeux nous proposons ici une définition de taille et de complexité pour les fonctions d'ordre supérieur de PCF, et plus généralement pour tout processus calculatoire assimilable à une certaine classe de jeux séquentiels.

Preuves, programmes et systèmes

Mardi 2 avril 2019, 10 heures 30, Salle 3052

**Jérémy Dubut** (NII, Tokyo) *Categorical approaches to bisimilarity*

Preuves, programmes et systèmes

Jeudi 28 mars 2019, 10 heures 30, Salle 3052

**Thomas Leventis** (Univ. Bologna (Italy)) *Taylor expansion of probabilistic lambda-terms*

Preuves, programmes et systèmes

Jeudi 21 mars 2019, 10 heures 30, Salle 3052

**Paolo Pistone** (Univ. Tubingen) *Quelques résultats sur l'équivalence des preuves dans la logique linéaire du second ordre*

Font partie de ces sémantiques “effaçantes” les sémantiques cohérente et rélationnelle, ainsi que la sémantique dinaturelle et la sémantique observationnelle. On présente des résultats sur l'équivalence des preuves dans ces sémantiques et on discute des applications en complexité dues à la possibilité de compresser les preuves. Une partie de ces travaux est issue d'une collaboration avec L. Tortora de Falco, T. Seiller et L.T.D. Nguyễn.

Preuves, programmes et systèmes

Jeudi 28 février 2019, 10 heures 30, Salle 3052

**François Bergeron** (UQAM) *Theory of species of structures and applications*

Preuves, programmes et systèmes

Mardi 26 février 2019, 10 heures 30, Salle 3052

**Eric Finster** (Inria - Nantes) *Higher Universal Algebra in Dependent Type Theory*

Preuves, programmes et systèmes

Jeudi 21 février 2019, 10 heures 30, Salle 3052

**Damiano Mazza** (CNRS) *Intersection Types and Runtime Errors in the Pi-Calculus*

Joint work with Ugo Dal Lago, Marc De Visme, Akira Yoshimizu

Preuves, programmes et systèmes

Jeudi 7 février 2019, 10 heures 30, Salle 3052

**Sandra Alves** *Linearisation of the lambda-calculus and its termination*

In this talk we will explore these previous works, discuss their relation and present some open problems regarding the termination of linearisation methods.

Preuves, programmes et systèmes

Jeudi 24 janvier 2019, 10 heures 30, Ens Lyon

**Seminaire Chocola** (Ens Lyon) *Non encore annoncé.*

Preuves, programmes et systèmes

Jeudi 10 janvier 2019, 10 heures 30, Salle 3052

**Aurore Alcolei** (Ens Lyon) *Concurrent strategies for Herbrand's theorem*

In this talk, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems. Closely related to expansion trees, the causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers. As furthermore these strategies can be composed we are able to interpret classical sequent proofs, yielding a compositional proof of Herbrand's theorem.

#### Année 2018

Preuves, programmes et systèmes

Jeudi 13 décembre 2018, 10 heures 30, ENS Lyon

**Journée Chocola** *ENS Lyon*

Preuves, programmes et systèmes

Jeudi 6 décembre 2018, 10 heures 30, Salle 3052

**Luc Pellissier** (IRIF) *Linear Implicative Algebras, towards a Brouwer-Heyting-Kolmogorov interpretation of linear logic*

In this ongoing work with Alexandre Miquel, we show how linear logic fits in this picture: we present a family of models, where certain computational principles are distinguished, and argue thata it provides a satisfactory meaning explanation of the connectives of (perfective) linear logic.

Preuves, programmes et systèmes

Jeudi 22 novembre 2018, 10 heures 30, Salle 3052

**Stéphane Graham-Lengrand** (LIX, CNRS) *The intuitionistic calculus that was discovered 6 times*

Preuves, programmes et systèmes

Jeudi 15 novembre 2018, 11 heures, Salle 3052 + Amphi Turing + 1016

**Eric Tanter, Flavien Breuvart, Shane Mansfield & Xavier Leroy** (Chocola meeting in Paris) *Salidou's day*

Gradual typing enables programming languages to seamlessly combine dynamic and static checking. Language researchers and designers have extended a wide variety of type systems to support gradual typing. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. Based on an understanding of gradual types as abstractions of static types, we have developed systematic foundations for gradual typing based on abstract interpretation, called Abstracting Gradual Typing (AGT for short). Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. In this talk, I will give a brief introduction to AGT in a simply-typed setting, and will then discuss recent work on a gradual counterpart of System F that enforces relational parametricity, even in the presence of imprecise types.

14:00 – 15:00 Flavien Breuvart (Université Paris 13) - Invited talk: Graded Types Parametricity : Principles and Application to Abstract Interpretation

In this talk, we will briefly present the yet-to-start project CoGITARe, which aims at developing further graded types expressivity and inference in order to use them to perform abstract interpretations. In a second time, we give an historic on graded type systems and their expressivity. Then, we will see that this expressivity is limited by a lake of dependency/parametricity. We will thus explore two ongoing research directions that adds two very different kind of parametricity to graded types. (The provocative title should only be taken as a joke. Despite their apparent similitudes, this work and Éric Tanter's have vastly different objectives and involved different issues and techniques. In particular, notice that gradual and graded types are fundamentally different.)

15:30 – 16:30 Shane Mansfield (Univ. of Oxford) - Invited talk: An overview of empirical models

Empirical models are a way of formalising data that arises in physical experiments. They were first proposed by Abramsky and Brandenburger as part of a framework to analyse fundamentally non-classical phenomena in quantum systems. Conveniently from a computer science perspective, they abstract away from the mathematical baggage of quantum theory and instead allow the key phenomena to be characterised purely as features of empirical data. After introducing the basic framework I will discuss some more recent results and developments, drawing on joint work with a number of collaborators. In particular: quantum computations can simply be modelled as classical computations with the additional ability to interact with a resource empirical model; quantitative measures of non-classicality can be shown to relate directly to some basic quantum-over-classical computational advantages; and the beginnings of a category-theoretic approach to reasoning about empirical models have emerged.

18:00 – 19:00 Xavier Leroy - Lecture: Leçon inaugurale au Collège de France

This is not part of the CHoCoLa day, but you might be interested in attending! See https://www.college-de-france.fr/site/xavier-leroy/inaugural-lecture-2018-11-15-18h00.htm

The meeting will take place in Bâtiment Sophie Germain, here. We will first gather at the 3rd floor of the building, for a breakfast. We will then move for the talk of the morning (11.00-12.30) to Amphi Turing. We will have lunch in room 3052 In the afternoon (14h-16h30), we will be in room 1016

Preuves, programmes et systèmes

Vendredi 9 novembre 2018, 9 heures 30, Salle 3052

**Pôle Preuves, Programmes Et Systèmes** *Journées 2018*

Preuves, programmes et systèmes

Jeudi 8 novembre 2018, 9 heures 30, Salle 3052

**Pôle Preuves, Programmes Et Systèmes** *Journées 2018*

Preuves, programmes et systèmes

Jeudi 25 octobre 2018, 10 heures 30, Salle 3052

**Carlo Spaccasassi** (Microsoft Research Cambridge, Cambridge (United Kingdom)) *Type-Based Analysis for Session Inference*

Preuves, programmes et systèmes

Jeudi 4 octobre 2018, 10 heures 30, Salle 3052

**Adrien Guatto** (IRIF) *Towards A General Guarded Lambda-Calculus*

Preuves, programmes et systèmes

Jeudi 27 septembre 2018, 10 heures 30, Salle 3052

**Thomas Streicher** (TU Darmstadt) *Simplicial sets inside cubical sets*

Abstract: Voevodsky's model of the Univalence Axion in simplicial sets is not constructive as shown by Coquand et al. To avoid this problem Cohen, Coquand, Huber, Moertberg have constructed in Cubical Sets a model of a Cubical Type Theory which has computational meaning.

We show that simplicial sets form a subtopos of cubical sets which allows one to contructively reason in the latter about the former.

Preuves, programmes et systèmes

Jeudi 5 juillet 2018, 10 heures 45, Salle 3052

**Jeremy Dubut** (National Institute of Informatics Tokyo, Japan) *Higher-Dimensional Automata*

Preuves, programmes et systèmes

Jeudi 28 juin 2018, 10 heures 30, Salle 3052

**Olivier Hermant** (CRI, Mines ParisTech) *Intersection Types in Deduction Modulo Theory*

We show that our rewrite system is terminating and that the conversion rule respects weak versions of invertibility of the arrow and of quantifiers. This requires additional care, in particular in the treatment of the latter. Then we study proof reduction, and show that every typable proof term is strongly normalizable and vice-versa.

Preuves, programmes et systèmes

Jeudi 31 mai 2018, 10 heures 30, Salle 3052

**Olivier Laurent** (ENS Lyon) *Balade entre logiques linéaires classiques et intuitionnistes*

Preuves, programmes et systèmes

Jeudi 29 mars 2018, 14 heures, Salle 3052

**Valentin Blot** (LRI) *Realizability: denotational semantics for correctness*

Preuves, programmes et systèmes

Jeudi 29 mars 2018, 10 heures 30, Salle 3052

**Guilhem Jaber** (LIP) *Model-checking contextual equivalence of higher-order programs with references.*

After introducing the notion of contextual equivalence, we will see on some examples why it is hard to prove such equivalences (reentrant calls, private states). As we will see, such examples can be found in many different programming languages.

Then, we will introduce SyTeCi, a tool to automatically check such equivalences. This tool is based on a reduction of the problem of contextual equivalence of two programs to the problem of reachability of “error states” in transition systems of memory configurations.

Contextual equivalence being undecidable (even in a finitary setting), so does the non-reachability problem for such transition systems. However, one can apply model-checking techniques (predicate abstraction, summarization of pushdown systems) to check non-reachability via some approximations. This allows us to prove automatically many non-trivial examples of the literature, that could only be proved by hand before. We will end this talk by the presentation of a prototype implementing this work.

Preuves, programmes et systèmes

Jeudi 22 février 2018, 10 heures 30, Salle 3052

**Pierre-Marie Pédrot** (Max Planck Institute for Software Systems, Saarbrücken, Germany) *Failure is Not an Option, or The Curry-Howard-Shadok correspondence*

Alas! The right to fail succeeds a tad too much, insofar as the resulting Shadock type theory is logically inconsistent. Not being impressed in any way, we put order into this madness by requiring that no exception should ever reach toplevel, thanks to a clever use of a variant of Bernardy-Lasson syntactic parametricity. While the former model can be thought of as Friedman A-translation applied to CIC, the latter is no more than a principled variant of Kreisel's modified realizability that scales to dependent types. In particular, it readily gives a model of CIC that still has canonicity, strong normalization and decidable type-checking, while featuring new principles typical of modified realizability such as the independence of premises and unprovability of Markov's principle.

https://www.pédrot.fr/articles/exceptional.pdf

Preuves, programmes et systèmes

Jeudi 15 février 2018, 10 heures 30, Salle 3052

**Prakash Panangaden** (McGill University) *Topology, Order and Causal Structure*

In a remarkable example of serendipity, order theory has been developed by computer scientists and mathematicians in order to capture computability concepts. Dana Scott developed a notion of a continuous lattice or continuous poset with a view to capturing computability as continuity with a suitable topology that has come to be known as the Scott topology. This subject has acquired the name of ``domain theory.''

We applied domain theory to the problem of reconstructing the spacetime topology from the order and came up with a number of results about reconstruction of spacetime structure from just a countable dense set.

We prove that a globally hyperbolic spacetime with its causality relation is a bicontinuous poset whose interval topology is the manifold topology. From this one can show that from only a countable dense set of events and the causality relation, it is possible to reconstruct a globally hyperbolic spacetime in a purely order theoretic manner. The ultimate reason for this is that globally hyperbolic spacetimes belong to a category that is equivalent to a special category of domains called interval domains.

This was joint work with Keye Martin of Naval Research Laboratories.

Preuves, programmes et systèmes

Jeudi 8 février 2018, 10 heures 30, Salle 3052

**Vincent Laporte** (IMDEA Software) *Provably secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”*

We consider the problem of preserving side-channel countermeasures by compilation for cryptographic “constant-time”, a popular countermeasure against cache-based timing attacks. We present a general method, based on the notion of 2-simulation, for proving that a compilation pass preserves the constant-time countermeasure. Using the Coq proof assistant, we verify the correctness of our method and of several representative instantiations.

Joint session Verification/PPS

Preuves, programmes et systèmes

Jeudi 8 février 2018, 10 heures 30, Salle 3052

**Séminaire Chocola** (ENS Lyon) *Rencontres Chocola de Février: Prakash Panangaden, Justin Hsu & Thomas Ehrhard*

10:30 – 12:00

Prakash Panangaden (Mc Gill University, Canada) Quantitative Equational Logic

14:00 – 15:00

Justin Hsu (University College London, UK) From Couplings to Probabilistic Relational Program Logics

15:30 – 16:30

Thomas Ehrhard (IRIF, Univ. Paris Diderot) Stable and measurable functions on positive cones: a model of probabilistic functional languages with continuous types

Preuves, programmes et systèmes

Jeudi 25 janvier 2018, 10 heures 30, Salle 3052

**Justin Hsu** (University College of London) *From Couplings to Probabilistic Relational Program Logics*

Bio: Justin Hsu is a post-doctoral researcher at the University College of London. He obtained his graduate degree from the University of Pennsylvania. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory.

#### Année 2017

Preuves, programmes et systèmes

Jeudi 14 décembre 2017, 10 heures 30, ENS Lyon

**Séminaire Chocola** *ENS Lyon*

Preuves, programmes et systèmes

Jeudi 14 décembre 2017, 10 heures 30, Salle 3052

**Juliusz Chroboczek** (IRIF, Université Paris Diderot) *Homenet, l'IETF, et le processus de normalisation*

Cet exposé est une version étendue et légèrement censurée de l'exposé que j'ai donné aux Journées PPS le 12 octobre 2017.

Preuves, programmes et systèmes

Jeudi 7 décembre 2017, 10 heures 30, Salle 3052

**Charles Grellois** (Université Aix-Marseille) *Linearity in Higher-Order Recursion Schemes*

In general, the complexity of the HOMC problem is n-EXPTIME, where n is the order of the HORS of interest. In this talk, we explain that we can refine this complexity measure: motivated by linear logic, we introduce *linear* HORS and a linear-nonlinear model of automaton checking fragments of MSO. We then show that HOMC is in fact n-EXPTIME complete for n the *linear* order of the linear HORS generating the tree of interest. We believe that this explains why HOMC, in spite of its huge theoretical complexity, has been successfully used in practice by Kobayashi's team.

This linear framework allows to reprove in a much simpler way three existing results extending the usual HOMC problem, and notably to deal with call-by-value programs in a smooth way (the usual HOMC approach considering call-by-name).

This is joint work with Pierre Clairambault and Andrzej Murawski.

Preuves, programmes et systèmes

Jeudi 23 novembre 2017, 10 heures 30, Salle 3052

**Simon Castellan** (Imperial College) *The parallel intensionally fully abstract model for PCF*

This talk focuses on the deterministic case. I will first introduce the concurrent strategies and their composition, in the existing linear setting. I will then present our extension to nonlinearity using copy indices and symmetry to represent uniformity. I will then present our notions of concurrent innocence & well-bracketing, to finish on our result of intensional full abstraction for PCF. Time permitting, I will discuss extensions of this result to non-angelic nondeterminism and probabilities.

Preuves, programmes et systèmes

Jeudi 9 novembre 2017, 10 heures 30, ENS Lyon

**Séminaire Chocola** *ENS LYon*

Preuves, programmes et systèmes

Jeudi 19 octobre 2017, 10 heures 30, Salle 3052

**Martin Hyland** (DPMMS, University of Cambridge) *Understanding Computation in Game Semantics*

Preuves, programmes et systèmes

Jeudi 15 juin 2017, 10 heures 30, Salle 3052

**Samuele Giraudo** (Paris-Est Marne-la-Vallée) *Découpage d'associativité généralisé*

Preuves, programmes et systèmes

Mardi 9 mai 2017, 14 heures, Salle 3052

**Valentin Blot** (Queen Mary University, London) *An interpretation of system F through bar recursion*

Preuves, programmes et systèmes

Jeudi 27 avril 2017, 10 heures 30, Salle 3052

**Bérénice Delcroix-Oger** (Institut de Mathématiques de Toulouse) *Des arbres sans ambiguités*

Preuves, programmes et systèmes

Jeudi 27 avril 2017, 14 heures, Salle 3052

**Jeremy Siek** (Indiana University) *The state of the art in gradual typing*

Jeremy Siek is an Associate Professor at Indiana University Bloomington. Jeremy's areas of research include programming language design, type systems, mechanized theorem proving using proof assistants, and optimizing compilers. Jeremy's Ph.D. thesis explored foundations for constrained templates, aka the “concepts” proposal for C++. Prior to that, Jeremy developed the Boost Graph Library, a C++ generic library for graph algorithms and data structures. Jeremy post-doc'd at Rice University where he developed the idea of gradual typing: a type system that integrates both dynamic and static typing in the same programming language. Jeremy is currently working on a gradually-typed version of Python. Jeremy received the NSF CAREER award to fund his project: “Bridging the Gap Between Prototyping and Production”. Jeremy was also twice awarded a Distinguished Visiting Fellowship from the Scottish Informatics & Computer Science Alliance.

Preuves, programmes et systèmes

Jeudi 20 avril 2017, 10 heures 30, Salle 3052

**Jamie Vicary** (Univ. of Oxford) *Formalizing Compositional Proofs*

Web site: https://ncatlab.org/nlab/show/Globular Paper: https://arxiv.org/abs/1610.06908

Preuves, programmes et systèmes

Jeudi 30 mars 2017, 10 heures, Salle 3052

**Giovanni Bernardi** (IRIF) *Un, personne et cent mille: a meta theory for testing equivalences?*

Preuves, programmes et systèmes

Jeudi 30 mars 2017, 11 heures 15, Salle 3052

**Daniela Petrisan** (IRIF) *Hybrid set-vector automata from a category-theoretic perspective*

We take a category-theoretic approach, which provides a neat understanding of minimisation. It is well known that category theory offers a unifying view of some automata theory results. For example, minimisation of deterministic automata (over finite words) and Shützenberger’s automata weighted over fields, arise from the same categorical reasons.

In the first part of the talk, I will discuss about how to model and minimise automata in categories. Traditionally, automata are seen either as algebras for a functor plus a final map, possibly in a monoidal category, or as coalgebras for a functor plus an initial map. We propose yet another view of automata as functors from an input category to an output category.

The new hybrid set-vector automata can be modelled by taking the output category to be a free-colimit completion of the category of finite-dimensional vector spaces under a certain class of colimits.

This is joint work with Thomas Colocombet.

Preuves, programmes et systèmes

Jeudi 23 mars 2017, 10 heures 30, Salle 3052

**Thomas Leventis** (Institut de Mathématiques de Marseille) *Full Abstraction of the Probabilistic Böhm Trees*

The solvability has a natural extension, which is the convergence probability, hence two terms are observationally equivalent if they have the same convergence probability under any context. There is also a simple way to define probabilistic Bohm trees, as we can associate to any term a subprobability distribution over head normal forms. But it is not obvious that these generalizations of the deterministic notions are still equivalent. In this talk we will show how to prove that probabilistic Böhm trees actually form a model, and how to get a separability result to ensure this model is fully abstract.

Preuves, programmes et systèmes

Jeudi 16 mars 2017, 10 heures 30, Salle 3052

**Charles Grellois** (INRIA - Univ. Bologna (Italie)) *Verifying properties of functional programs: from the deterministic to the probabilistic case*

Preuves, programmes et systèmes

Jeudi 23 février 2017, 10 heures 30, Salle 3052

**Marcelo Fiore** (University of Cambridge) *An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures*

[1] J.Baez and J.Dolan. Higher-Dimensional Algebra III. n-Categories and the Algebra of Opetopes. Advances in Mathematics 135, pages 145-206, 1998.

[2] M.Fiore, G.Plotkin and D.Turi. Abstract syntax and variable binding. In 14th Logic in Computer Science Conf. (LICS'99), pages 193-202. IEEE, Computer Society Press, 1999.

[3] M.Fiore. Second-order and dependently-sorted abstract syntax. In Logic in Computer Science Conf. (LICS'08), pages 57–68. IEEE, Computer Society Press, 2008.

[4] M.Fiore, N.Gambino, M.Hyland, and G.Winskel. The cartesian closed bicategory of generalised species of structures. In J. London Math. Soc.}, 77:203-220, 2008.

[5] S.Szawiel and M.Zawadowski. The web monoid and opetopic sets. In arXiv:1011.2374 [math.CT], 2010.

Preuves, programmes et systèmes

Jeudi 26 janvier 2017, 10 heures 30, Salle 3052

**Tarmo Uustalu** (Tallinn University of Technology) *Dynamic programming and coalgebras with sharing*

In this talk, we present a generic framework for doing so and demonstrate it in action on two textbook examples of dynamic programming - Fibonacci and edit distance. We describe sharing opportunity patterns with systems of equations between node addresses. A technique from term rewriting systems, namely Knuth-Bendix completion, gives us unique normal forms for node addresses. A dag is represented as a spanning tree whose nodes are defined by addresses in normal form. Mathematically, the function taking an input for our function of interest into a call tree is a comonad coalgebra, node addresses are coterms and equations are coequations.

A Haskell implementation of this framework uses circular programming and a generic implementation of derivatives of functors.

We view this work as a showcase of how basic algorithmics and more advanced category theory can interact in a mutually beneficial way.

This joint work with Nicolas Wu, University of Bristol.

Preuves, programmes et systèmes

Mardi 10 janvier 2017, 11 heures, Salle 3052

**Camell Kachour** (IRIF) *Sur des modèles algébriques d'infini-n-catégories faibles cubiques*

#### Année 2016

Preuves, programmes et systèmes

Jeudi 1 décembre 2016, 10 heures 30, Salle 3052

**Julien Lange** (Imperial College) *Building Graphical Choreographies From Communicating Machines: Principles and Applications*

Preuves, programmes et systèmes

Jeudi 24 novembre 2016, 10 heures 30, Salle 3052

**Thibaut Balabonski** (LRI, Université Paris Sud) *Optimisation de programmes C++ concurrents*

Preuves, programmes et systèmes

Jeudi 17 novembre 2016, 10 heures 30, Salle 3052

**Bruno Barras** *Exposé repoussé à début 2017*

Preuves, programmes et systèmes

Jeudi 3 novembre 2016, 10 heures 30, Salle 3052

**Guilhem Jaber** (IRIF) *Operational Nominal Game Semantics*

Preuves, programmes et systèmes

Jeudi 6 octobre 2016, 10 heures 30, Salle 3052

**Giulio Manzonetto** (LIPN) *New Results on Morris's Observational Theory — The Benefits of Separating the Inseparable*

Preuves, programmes et systèmes

Jeudi 29 septembre 2016, 10 heures 30, Salle 3052

**Vincent Danos** (ENS) *Bayesian inversion by ω-complete cone duality*

Preuves, programmes et systèmes

Jeudi 2 juin 2016, 10 heures 30, Salle 3052

**Ugo Dal Lago** (Univ. Bologna) *Infinitary Lambda Calculi from a Linear Perspective*

Preuves, programmes et systèmes

Jeudi 21 avril 2016, 10 heures 30, Salle 3052

**Silvia Ghilezan** (Université de Novi Sad) *Preciseness of Subtyping on Intersection and Union Types*

We propose a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We prove then sound- ness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness.

This is a joint work with Mariangiola Dezani-Ciancaglini.

Preuves, programmes et systèmes

Mercredi 30 mars 2016, 10 heures 30, Salle 3052

**Guillaume Munch-Maccagnoni** (Cambridge Computer lab) *Enriched-adjunction models and polarisation for modelling effects and resources*

I will present “linear call-by-push-value” enriched-adjunction models refining call-by-push-value models of effects and linear/non-linear models of linear logic, with higher-order functions, sums, and resource modalities, together with a theorem lifting linear models into cartesian ones. I will also present computational interpretations of these models as intuitionistic (linear) logics (LJ/ILL) where the order of evaluation matters, in the form of polarised calculi that satisfy usual properties of Barendregt-style lambda-calculus, and that have sound and coherent interpretations in the previous models. This suggests an approach to modelling proofs and programs with direct models and calculi.

Preuves, programmes et systèmes

Jeudi 24 mars 2016, 10 heures 30, Salle 3052

**Pawel Sobocinski** (University of Southampton) *Non encore annoncé.*

Preuves, programmes et systèmes

Jeudi 10 mars 2016, 10 heures 30, Salle du Conseil

**Thomas Seiller** (Department of Computer Science, University of Copenhagen - DIKU) *Complexity Constraints as Group Actions*

The origins of the techniques can be traced to Girard's “geometry of interaction” (GoI) program using von Neumann algebras and the recent GoI-inspired results in complexity. However, this approach reaches its full strength when using the more combinatorial setting of Interaction Graphs models of (fragments of) linear logic. Using techniques akin to game semantics (with a bit of measure theory), we are able to characterise (predicate) complexity classes as the set of programs/proofs interpretations of type Pred[m] := Nat ⇒ Bool. These models are parametrised by a group of measure-preserving maps m (equivalently, by a measurable group action) and provide the first sketches of a conjectured correspondence between measurable group actions and complexity constraints.

Preuves, programmes et systèmes

Jeudi 14 janvier 2016, 10 heures 30, Salle 3052

**Amar Hadzihasanovic** (Oxford University) *String diagrams and the algebra of entanglement*