Inria project-team $\pi r^2$ (Inria)

Thematic team Algebra and computation

Thematic team Analysis and conception of systems

Thematic team Proofs and programs

## Proofs, programs and systems

#### Day, hour and place

Thursday at 10:30am, room 3052

The calendar of events (iCal format).

In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.

#### Contact(s)

To receive talk announcements for the PPS seminar, please send an email to sympa@listes.irif.fr with “subscribe seminaire-pps YourFirstname YourLastname” as a title and an empty body.

### Next talk

Proofs, programs and systems

Thursday June 22, 2023, 10:30AM, Room: TBA

**Hall Hands On Deck** *AG*

### Previous talks

#### Year 2023

Proofs, programs and systems

Friday May 26, 2023, 9:30AM, Amphi 9e Halle aux Farines

**All Hands On Deck** (PPS pole) *Journées PPS 2023*

Proofs, programs and systems

Thursday May 25, 2023, 9:30AM, Amphi 9e Halle aux Farines

**All Hands On Deck** (pole PPS) *Journées PPS 2023*

Proofs, programs and systems

Thursday April 13, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**Giulio Manzonetto** (Université Sorbonne Paris Nord) *The Lambda Calculus - 40 Years Later*

Proofs, programs and systems

Thursday March 30, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**Romain Pascual** (Université Paris-Saclay) *Graph transformation for reasoning about geometric modeling operations*

Proofs, programs and systems

Thursday March 23, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**Giulio Manzonetto** *Postponed to Apil 13th.*

Proofs, programs and systems

Thursday March 16, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**Adrien Durier** (Université Paris-Saclay) *Open call-by-value and concurrency*

Proofs, programs and systems

Thursday March 9, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**Ghyselen Alexis** (Università di Bologna) *Choices via algebraic operations and stateful computations*

In this talk, I will present a joint work with Ugo Dal Lago and Francesco Gavazzo on how algebraic operations, and handlers, can support decision-making abstractions in functional programs: a user can invoke an operation to resolve choices without implementing the underlying selection mechanism, and can give feedback by way of rewards. We differ from some recently proposed approach to the problem based on the selection monad, by Abadi and Plotkin, as we express the underlying selection mechanism with efficient algorithms implemented by a set of handlers. I will first introduce algebraic effects and handlers, then present the selection monad approach for choices, and our approach, based on stateful computations (or equivalently comodels). Both the theoretical and practical aspects will be examined, and I will show the practical efficiency of our approach compared to the selection monad. Finally, I will focus on how our work can actually be implemented in a modular way on a concrete language with handlers and how we can use expressive type systems to obtain safety properties, especially ensuring a high-degree of modularity and a sound usage of algebraic operations.

Proofs, programs and systems

Thursday February 23, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**Francesco Gavazzo** (University of Pisa) *Computational Effects From a Relational Angle*

Proofs, programs and systems

Tuesday February 14, 2023, 11AM, Salle 3052 & online (Zoom link)

**Benoît Valiron** (CentraleSupélec) *Complete Equational Theories for Linear Optical and Quantum Circuits*

We shall first present our proposed equational theory for linear optical circuits. We shall then discuss how the semantics of both kind of circuits differ, and how to relate them using controlled-gates. The discussion will drive is to the completeness result for quantum circuits, based on the one for linear optical circuits.

Joint session with the Algorithmes et complexité seminar series.

Proofs, programs and systems

Thursday February 9, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**Clément Blaudeau** (INRIA Paris, CAMBIUM Project-Team) *Retrofitting OCaml modules*

Proofs, programs and systems

Thursday January 26, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**George Metcalfe** (University of Bern) *Deciding equations in ordered groups and ordered monoids*

This talk will be about deciding equations in various classes of ordered groups and ordered monoids, and how this relates to deciding if there exist orders on free groups and monoids satisfying finitely many inequalities.

Removing the inverse operation from any lattice-ordered group (l-group) yields a distributive lattice-ordered monoid (l-monoid), but not every distributive l-monoid admits a group structure. Indeed, every distributive l-monoid is a (possibly finite) pointwise-ordered monoid of order-preserving maps on a chain, whereas every l-group is a pointwise-ordered group of order-preserving permutations on a chain and must be either trivial or infinite.

We will see that the equational theory of distributive l-monoids is decidable and coincides with the equational theory of l-groups without inverses, and hence, by eliminating inverses, that the equational theory of l-groups is also decidable. This contrasts with the fact that there are inverse-free equations that are satisfied by all totally ordered abelian groups but not all totally ordered commutative monoids, and the decidability of the equational theory of the latter is open.

Proofs, programs and systems

Thursday January 12, 2023, 10:30AM, Salle 3052 & online (Zoom link)

**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).

#### Year 2022

Proofs, programs and systems

Thursday December 15, 2022, 10:30AM, Salle 3052 & online (Zoom link)

**Davide Barbarossa** (Università di Bologna) *Lambda-calculus goes to the tropics*

Proofs, programs and systems

Thursday December 8, 2022, 10:30AM, Salle 3052 & online (Zoom link)

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

Proofs, programs and systems

Thursday December 1, 2022, 10:30AM, Salle 3052 & online (Zoom link)

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

Proofs, programs and systems

Thursday November 10, 2022, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday October 13, 2022, 10:30AM, Salle 3052 & online (Zoom link)

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

Proofs, programs and systems

Thursday October 6, 2022, 10AM, Salle 3052

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

Proofs, programs and systems

Thursday September 22, 2022, 10:30AM, ENS Lyon

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

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

Proofs, programs and systems

Monday September 19, 2022, 11AM, 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.

Proofs, programs and systems

Wednesday July 13, 2022, 2:30PM, 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.

Proofs, programs and systems

Tuesday July 12, 2022, 2:30PM, 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.

Proofs, programs and systems

Monday July 11, 2022, 2:30PM, 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.

Proofs, programs and systems

Thursday June 23, 2022, 10:30AM, 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).

Proofs, programs and systems

Thursday June 16, 2022, 10:30AM, Salle 3052 & online (Zoom link)

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

Proofs, programs and systems

Thursday June 9, 2022, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday June 2, 2022, 10:30AM, Online (Zoom link)

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

Proofs, programs and systems

Thursday May 19, 2022, 10:30AM, 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.

Proofs, programs and systems

Thursday May 12, 2022, 10:30AM, 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.

Proofs, programs and systems

Thursday May 5, 2022, 10:30AM, 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>.

Proofs, programs and systems

Thursday April 28, 2022, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday April 21, 2022, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday April 7, 2022, 10:30AM, 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/

Proofs, programs and systems

Thursday March 31, 2022, 10:30AM, Online

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

Proofs, programs and systems

Thursday March 24, 2022, 10:30AM, Online

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

Online at link (any password works)

Proofs, programs and systems

Thursday March 17, 2022, 10:30AM, 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)

Proofs, programs and systems

Thursday March 10, 2022, 10:15AM, On-line.

**Tba** *Séminaire CHOCOLA*

Proofs, programs and systems

Thursday March 3, 2022, 10:30AM, 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.

Proofs, programs and systems

Thursday February 17, 2022, 10:30AM, 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.

Proofs, programs and systems

Thursday January 27, 2022, 10:30AM, Room 3052 and virtual room at link (any password works)

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

Proofs, programs and systems

Thursday January 20, 2022, 10:15AM, 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.

Proofs, programs and systems

Thursday January 13, 2022, 10:30AM, 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)

#### Year 2021

Proofs, programs and systems

Thursday December 16, 2021, 10:30AM, 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.

Proofs, programs and systems

Friday December 10, 2021, 10:30AM, 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

Proofs, programs and systems

Thursday December 2, 2021, 10:30AM, 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.

Proofs, programs and systems

Thursday November 25, 2021, 10:30AM, Room 3052 and virtual room at link (any password works)

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

Proofs, programs and systems

Thursday November 18, 2021, 10:30AM, 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.

Proofs, programs and systems

Thursday October 21, 2021, 10:15AM, 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.

Proofs, programs and systems

Thursday July 1, 2021, 10AM, 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.

Proofs, programs and systems

Thursday June 24, 2021, 5PM, 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.

Proofs, programs and systems

Thursday June 17, 2021, 10AM, 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.

Proofs, programs and systems

Thursday June 10, 2021, 10:30AM, 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

Proofs, programs and systems

Thursday June 3, 2021, 3PM, 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.

Proofs, programs and systems

Thursday May 27, 2021, 10:30AM, Online at link (any password works)

**Xavier Rival** (École normale supérieure) *To be announced.*

(Joint work with Hugo Illous and Matthieu Lemerre.)

Proofs, programs and systems

Thursday May 20, 2021, 10AM, 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.

Proofs, programs and systems

Thursday May 6, 2021, 10AM, 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.

Proofs, programs and systems

Thursday April 29, 2021, 10:30AM, 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.

Proofs, programs and systems

Thursday April 22, 2021, 10AM, 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.

Proofs, programs and systems

Thursday April 1, 2021, 10:30AM, https://galene.org:8443/group/seminaire-pps

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

Proofs, programs and systems

Thursday April 1, 2021, 2PM, https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk

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

Proofs, programs and systems

Monday March 29, 2021, 2PM, https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk

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

Proofs, programs and systems

Tuesday March 23, 2021, 10:30AM, 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.

Proofs, programs and systems

Tuesday March 23, 2021, 2PM, https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-tje-nwj-dtk

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

Proofs, programs and systems

Monday March 22, 2021, 2PM, https://galene.org:8443/group/seminaire-pps

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

Proofs, programs and systems

Thursday March 4, 2021, 10:30AM, 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)

Proofs, programs and systems

Thursday February 25, 2021, 10:30AM, 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)

Proofs, programs and systems

Wednesday February 24, 2021, 2PM, 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.

Proofs, programs and systems

Thursday February 18, 2021, 10:30AM, 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)

Proofs, programs and systems

Friday February 12, 2021, 2PM, 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”.

Proofs, programs and systems

Thursday February 11, 2021, 10:30AM, Online

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

Virtual room at link (any password works)

Proofs, programs and systems

Thursday February 4, 2021, 10:30AM, Online

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

Virtual room at link (any password works)

Proofs, programs and systems

Thursday January 28, 2021, 10:30AM, 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)

#### Year 2020

Proofs, programs and systems

Thursday December 17, 2020, 10:30AM, 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)

Proofs, programs and systems

Thursday December 3, 2020, 10:30AM, 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)

Proofs, programs and systems

Thursday November 26, 2020, 10:30AM, Online

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

Virtual room at link (any password works)

Proofs, programs and systems

Thursday November 19, 2020, 10:30AM, 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)

Proofs, programs and systems

Thursday November 12, 2020, 10:30AM, Online

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

Link (any password works)

Proofs, programs and systems

Thursday November 5, 2020, 10:30AM, Online

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

Proofs, programs and systems

Thursday October 29, 2020, 3PM, 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.

Proofs, programs and systems

Thursday October 22, 2020, 10:30AM, Online at this link

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

Proofs, programs and systems

Thursday October 15, 2020, 10AM, Online

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

Proofs, programs and systems

Thursday October 8, 2020, 10:30AM, 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

Proofs, programs and systems

Thursday October 1, 2020, 10:30AM, 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

Proofs, programs and systems

Thursday June 18, 2020, 3:30PM, 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.

Proofs, programs and systems

Thursday June 11, 2020, 3:30PM, Online

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

Proofs, programs and systems

Wednesday June 10, 2020, 3PM, 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.

Proofs, programs and systems

Tuesday June 9, 2020, 4PM, 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.

Proofs, programs and systems

Thursday May 28, 2020, 3:30PM, 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.

Proofs, programs and systems

Thursday May 14, 2020, 3:30PM, 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.

Proofs, programs and systems

Thursday May 7, 2020, 3:30PM, Online

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

Proofs, programs and systems

Thursday April 30, 2020, 3:30PM, 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.

Proofs, programs and systems

Thursday April 9, 2020, 3:30PM, Online

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

Proofs, programs and systems

Thursday March 26, 2020, 2PM, 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!

Proofs, programs and systems

Thursday February 13, 2020, 10:45AM, 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**.)

Proofs, programs and systems

Thursday January 23, 2020, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday January 16, 2020, 10:30AM, 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.

Proofs, programs and systems

Friday January 10, 2020, 10AM, 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.)

#### Year 2019

Proofs, programs and systems

Thursday December 12, 2019, 10:30AM, École normale supérieure de Lyon

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

Proofs, programs and systems

Thursday November 28, 2019, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday November 21, 2019, 10:30AM, 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.

Proofs, programs and systems

Thursday November 14, 2019, 10:30AM, École normale supérieure de Lyon

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

Proofs, programs and systems

Thursday October 17, 2019, 10:30AM, École normale supérieure de Lyon

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

Proofs, programs and systems

Thursday October 3, 2019, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday September 26, 2019, 10:30AM, École normale supérieure de Lyon

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

Proofs, programs and systems

Monday September 2, 2019, 9:30AM, Amphithéâtre Turing

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

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

Proofs, programs and systems

Thursday June 20, 2019, 10:30AM, Salle 3052

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

Proofs, programs and systems

Wednesday June 19, 2019, 2:30PM, Salle 3052

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

Joint work with Naohiko Hoshino

Proofs, programs and systems

Monday June 17, 2019, 11AM, 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.

Proofs, programs and systems

Thursday June 13, 2019, 10:30AM, Salle 3052

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

Joint work with Koko Muroya and Todd Waugh Ambridge.

Proofs, programs and systems

Tuesday June 11, 2019, 11AM, Salle 3052

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

Proofs, programs and systems

Thursday June 6, 2019, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday May 16, 2019, 10:30AM, 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.)

Proofs, programs and systems

Thursday May 2, 2019, 10:30AM, 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.

Proofs, programs and systems

Tuesday April 2, 2019, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday March 28, 2019, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday March 21, 2019, 10:30AM, 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.

Proofs, programs and systems

Thursday February 28, 2019, 10:30AM, Salle 3052

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

Proofs, programs and systems

Tuesday February 26, 2019, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday February 21, 2019, 10:30AM, 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

Proofs, programs and systems

Thursday February 7, 2019, 10:30AM, 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.

Proofs, programs and systems

Thursday January 24, 2019, 10:30AM, Ens Lyon

**Seminaire Chocola** (Ens Lyon) *To be announced.*

Proofs, programs and systems

Thursday January 10, 2019, 10:30AM, 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.

#### Year 2018

Proofs, programs and systems

Thursday December 13, 2018, 10:30AM, ENS Lyon

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

Proofs, programs and systems

Thursday December 6, 2018, 10:30AM, 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.

Proofs, programs and systems

Thursday November 22, 2018, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday November 15, 2018, 11AM, 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

Proofs, programs and systems

Friday November 9, 2018, 9:30AM, Salle 3052

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

Proofs, programs and systems

Thursday November 8, 2018, 9:30AM, Salle 3052

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

Proofs, programs and systems

Thursday October 25, 2018, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday October 4, 2018, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday September 27, 2018, 10:30AM, 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.

Proofs, programs and systems

Thursday July 5, 2018, 10:45AM, Salle 3052

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

Proofs, programs and systems

Thursday June 28, 2018, 10:30AM, 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.

Proofs, programs and systems

Thursday May 31, 2018, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday March 29, 2018, 2PM, Salle 3052

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

Proofs, programs and systems

Thursday March 29, 2018, 10:30AM, 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.

Proofs, programs and systems

Thursday February 22, 2018, 10:30AM, 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

Proofs, programs and systems

Thursday February 15, 2018, 10:30AM, 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.

Proofs, programs and systems

Thursday February 8, 2018, 10:30AM, 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

Proofs, programs and systems

Thursday February 8, 2018, 10:30AM, 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

Proofs, programs and systems

Thursday January 25, 2018, 10:30AM, 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.

#### Year 2017

Proofs, programs and systems

Thursday December 14, 2017, 10:30AM, ENS Lyon

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

Proofs, programs and systems

Thursday December 14, 2017, 10:30AM, 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.

Proofs, programs and systems

Thursday December 7, 2017, 10:30AM, 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.

Proofs, programs and systems

Thursday November 23, 2017, 10:30AM, 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.

Proofs, programs and systems

Thursday November 9, 2017, 10:30AM, ENS Lyon

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

Proofs, programs and systems

Thursday October 19, 2017, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday June 15, 2017, 10:30AM, Salle 3052

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

Proofs, programs and systems

Tuesday May 9, 2017, 2PM, Salle 3052

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

Proofs, programs and systems

Thursday April 27, 2017, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday April 27, 2017, 2PM, 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.

Proofs, programs and systems

Thursday April 20, 2017, 10:30AM, 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

Proofs, programs and systems

Thursday March 30, 2017, 10AM, Salle 3052

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

Proofs, programs and systems

Thursday March 30, 2017, 11:15AM, 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.

Proofs, programs and systems

Thursday March 23, 2017, 10:30AM, 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.

Proofs, programs and systems

Thursday March 16, 2017, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday February 23, 2017, 10:30AM, 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.

Proofs, programs and systems

Thursday January 26, 2017, 10:30AM, 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.

Proofs, programs and systems

Tuesday January 10, 2017, 11AM, Salle 3052

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

#### Year 2016

Proofs, programs and systems

Thursday December 1, 2016, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday November 24, 2016, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday November 17, 2016, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday November 3, 2016, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday October 6, 2016, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday September 29, 2016, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday June 2, 2016, 10:30AM, Salle 3052

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

Proofs, programs and systems

Thursday April 21, 2016, 10:30AM, 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.

Proofs, programs and systems

Wednesday March 30, 2016, 10:30AM, 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.

Proofs, programs and systems

Thursday March 24, 2016, 10:30AM, Salle 3052

**Pawel Sobocinski** (University of Southampton) *To be announced.*

Proofs, programs and systems

Thursday March 10, 2016, 10:30AM, 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.

Proofs, programs and systems

Thursday January 14, 2016, 10:30AM, Salle 3052

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