Équipe-projet INRIA $\pi r^2$

É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

#### Contact(s)

### Prochaines séances

Preuves, programmes et systèmes

Mardi 26 février 2019, 11 heures, Salle 3052

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

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*

### Séances passées

#### Année 2019

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.

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*

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*