É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

Le jeudi à 15h30, en ligne

Le calendrier des séances (format iCal).

Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.

#### Contact(s)

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

### Séances passées

#### Année 2021

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

Jeudi 4 mars 2021, 10 heures 30, Online

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

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

Virtual room at link (any password works)

Preuves, programmes et systèmes

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

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

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

Virtual room at link (any password works)

Preuves, programmes et systèmes

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

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

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

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

Preuves, programmes et systèmes

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

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

Joint session with the Combinatoire seminar.

Virtual room at link (any password works)

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

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

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

Virtual room at link (any password works)

Preuves, programmes et systèmes

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

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

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 28 janvier 2021, 10 heures 30, Online

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

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

Virtual room at link (any password works)

#### Année 2020

Preuves, programmes et systèmes

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

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

Virtual room at link (any password works)

Preuves, programmes et systèmes

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

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

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

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 26 novembre 2020, 10 heures 30, Online

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

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 19 novembre 2020, 10 heures 30, Online

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

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

Virtual room at link (any password works)

Preuves, programmes et systèmes

Jeudi 12 novembre 2020, 10 heures 30, Online

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

Link (any password works)

Preuves, programmes et systèmes

Jeudi 5 novembre 2020, 10 heures 30, Online

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

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

Jeudi 15 octobre 2020, 10 heures, Online

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

Preuves, programmes et systèmes

Jeudi 8 octobre 2020, 10 heures 30, Online

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

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

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

- Zeinab Galal: A Profonctorial Finiteness Semantics;

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

- Ada Vienot: tba

Preuves, programmes et systèmes

Jeudi 1 octobre 2020, 10 heures 30, Online

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

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

- El-Mehdi Cherradi: Preuves, programmes et homotopie

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

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

Preuves, programmes et systèmes

Jeudi 18 juin 2020, 15 heures 30, Online

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

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

Preuves, programmes et systèmes

Jeudi 11 juin 2020, 15 heures 30, Online

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

Preuves, programmes et systèmes

Mercredi 10 juin 2020, 15 heures, Online

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

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

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

Preuves, programmes et systèmes

Mardi 9 juin 2020, 16 heures, Online

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

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

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

Preuves, programmes et systèmes

Jeudi 28 mai 2020, 15 heures 30, Online

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

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

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

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

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

Preuves, programmes et systèmes

Jeudi 14 mai 2020, 15 heures 30, Online

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

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

Preuves, programmes et systèmes

Jeudi 7 mai 2020, 15 heures 30, Online

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

Preuves, programmes et systèmes

Jeudi 30 avril 2020, 15 heures 30, Online

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

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

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

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

Preuves, programmes et systèmes

Jeudi 9 avril 2020, 15 heures 30, Online

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

Preuves, programmes et systèmes

Jeudi 26 mars 2020, 14 heures, Online

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

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

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

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

This seminar will take place online. More information soon!

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

Jeudi 23 janvier 2020, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 16 janvier 2020, 10 heures 30, Salle 3052

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

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

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

Preuves, programmes et systèmes

Vendredi 10 janvier 2020, 10 heures, Salle 3014

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

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

(Joint session between the PPS and Verification seminars.)

#### Année 2019

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

Jeudi 28 novembre 2019, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 21 novembre 2019, 10 heures 30, Salle 3052

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

Jeudi 3 octobre 2019, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

Jeudi 20 juin 2019, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Mercredi 19 juin 2019, 14 heures 30, Salle 3052

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

Joint work with Naohiko Hoshino

Preuves, programmes et systèmes

Lundi 17 juin 2019, 11 heures, Salle 3052

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

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

Preuves, programmes et systèmes

Jeudi 13 juin 2019, 10 heures 30, Salle 3052

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

Joint work with Koko Muroya and Todd Waugh Ambridge.

Preuves, programmes et systèmes

Mardi 11 juin 2019, 11 heures, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 6 juin 2019, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 16 mai 2019, 10 heures 30, Salle 3052

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

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

(Joint work with Jules Chouquet.)

Preuves, programmes et systèmes

Jeudi 2 mai 2019, 10 heures 30, Salle 3052

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

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

Preuves, programmes et systèmes

Mardi 2 avril 2019, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 28 mars 2019, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 21 mars 2019, 10 heures 30, Salle 3052

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

Jeudi 24 janvier 2019, 10 heures 30, Ens Lyon

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

Preuves, programmes et systèmes

Jeudi 10 janvier 2019, 10 heures 30, Salle 3052

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

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

#### Année 2018

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

Jeudi 22 novembre 2018, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

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

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

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

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

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

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

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

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

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

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

Preuves, programmes et systèmes

Vendredi 9 novembre 2018, 9 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 8 novembre 2018, 9 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 25 octobre 2018, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 4 octobre 2018, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 27 septembre 2018, 10 heures 30, Salle 3052

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

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

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

Preuves, programmes et systèmes

Jeudi 5 juillet 2018, 10 heures 45, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 28 juin 2018, 10 heures 30, Salle 3052

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

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

Preuves, programmes et systèmes

Jeudi 31 mai 2018, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 29 mars 2018, 14 heures, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 29 mars 2018, 10 heures 30, Salle 3052

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

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

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

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

Preuves, programmes et systèmes

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

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

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

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

Preuves, programmes et systèmes

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

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

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

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

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

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

Preuves, programmes et systèmes

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

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

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

Joint session Verification/PPS

Preuves, programmes et systèmes

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

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

10:30 – 12:00

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

14:00 – 15:00

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

15:30 – 16:30

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

Preuves, programmes et systèmes

Jeudi 25 janvier 2018, 10 heures 30, Salle 3052

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

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

#### Année 2017

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

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

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

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

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

This is joint work with Pierre Clairambault and Andrzej Murawski.

Preuves, programmes et systèmes

Jeudi 23 novembre 2017, 10 heures 30, Salle 3052

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

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

Preuves, programmes et systèmes

Jeudi 9 novembre 2017, 10 heures 30, ENS Lyon

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

Preuves, programmes et systèmes

Jeudi 19 octobre 2017, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 15 juin 2017, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Mardi 9 mai 2017, 14 heures, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 27 avril 2017, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 27 avril 2017, 14 heures, Salle 3052

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

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

Preuves, programmes et systèmes

Jeudi 20 avril 2017, 10 heures 30, Salle 3052

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

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

Preuves, programmes et systèmes

Jeudi 30 mars 2017, 10 heures, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 30 mars 2017, 11 heures 15, Salle 3052

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

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

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

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

This is joint work with Thomas Colocombet.

Preuves, programmes et systèmes

Jeudi 23 mars 2017, 10 heures 30, Salle 3052

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

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

Preuves, programmes et systèmes

Jeudi 16 mars 2017, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

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

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

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

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

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

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

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

Preuves, programmes et systèmes

Jeudi 26 janvier 2017, 10 heures 30, Salle 3052

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

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

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

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

This joint work with Nicolas Wu, University of Bristol.

Preuves, programmes et systèmes

Mardi 10 janvier 2017, 11 heures, Salle 3052

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

#### Année 2016

Preuves, programmes et systèmes

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

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

Preuves, programmes et systèmes

Jeudi 24 novembre 2016, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 17 novembre 2016, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 3 novembre 2016, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 6 octobre 2016, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 29 septembre 2016, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 2 juin 2016, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

Jeudi 21 avril 2016, 10 heures 30, Salle 3052

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

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

This is a joint work with Mariangiola Dezani-Ciancaglini.

Preuves, programmes et systèmes

Mercredi 30 mars 2016, 10 heures 30, Salle 3052

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

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

Preuves, programmes et systèmes

Jeudi 24 mars 2016, 10 heures 30, Salle 3052

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

Preuves, programmes et systèmes

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

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

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

Preuves, programmes et systèmes

Jeudi 14 janvier 2016, 10 heures 30, Salle 3052

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