Équipe thématique Algèbre et calcul

Équipe-projet Inria Picube (Inria)

Équipe thématique Preuves et programmes

## Sémantique

#### Jour, heure et lieu

Le mardi / mercredi à 10h45, salle 3052

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)

### Prochaines séances

Sémantique

Mercredi 20 décembre 2023, 10 heures 45, Salle 3052

**Paige North** (Utrecht University) *Non encore annoncé.*

https://paigenorth.github.io/

Sémantique

Mercredi 10 janvier 2024, 10 heures 45, Salle 3052

**Aloÿs Dufour** (LIPN, Université Sorbonne Paris Nord) *Non encore annoncé.*

Sémantique

Mercredi 7 février 2024, 10 heures 45, Salle 3052

**Francesca Guffanti** (University of Luxembourg) *Non encore annoncé.*

### Séances passées

#### Année 2023

Sémantique

Mercredi 22 novembre 2023, 10 heures 45, Salle 3052, 3ème étage du bâtiment Sophie Germain

**Jérémy Ledent** (IRIF) *Simplicial Complex models for Distributed Computing*

Sémantique

Mercredi 15 novembre 2023, 10 heures 45, Salle 3052

**Davide Quadrellaro** (University of Helsinki) *Towards AECats for Team Semantics*

Sémantique

Mardi 14 novembre 2023, 9 heures 45, Salle 1007

**Rémy Cerda** (Université d'Aix-Marseille) *Uniformity and the Taylor expansion of infinitary λ-terms*

Séance à l'horaire exceptionnel de 9h45 à 11h

Sémantique

Mardi 7 novembre 2023, 10 heures 45, Salle 3052, 3ème étage du bâtiment Sophie Germain

**Masahiro Hamano** (NCKU, Taiwan) *A Measure-Theoretical Linear Exponential Comonad and its Double Glueing Lifting*

(i) A monoidai category of s-finite transition kernels is introduced and shown to have a linear exponential comonad. The s-finitness, recently rediscovered by Staton for probabilistic programming semantics, is a relaxation of the traditional sigma finiteness, allowing the retention of Fubini-Tonelli Theorem, which theorem guarantees the functorial monodical product. Our focus on s-finiteness lies in its ability to accommodate an exponential construction tailored in stochastic process. To achieve this, we employ Melliès-Tabareau-Tasson free exponential construction, utilising equalisers on monoidal symmetries and their limit, These equalisers and limit find instances in measure-theoretic exponential both on measurable spaces and on kernels. (ii) A continuous orthogonality of linear logic is formulated in terms of integral between measures and measurable functions. The orthogonality embodies a simple reciprocity on kernels actions on measurable functions and measures. Following Hyland-Schalik's double gluing construction with tight orthogonality, we show that the free exponential of (I) is lifted to the tight orthogonal category over the s-finite kernels. To achieve this lifting, we rely the coherence of the limit with equalisers imposed by MTT, This coherence is shown to be realised through the Lebesgue monotone convergence theorem. Note that both (i) and (ii) do not incorporate any closed structure for monoidal products in the continuous framework, making them inconclusive as a complete model of linear logic.

Sémantique

Mercredi 25 octobre 2023, 10 heures 45, Salle 3052, 3ème étage du bâtiment Sophie Germain

**Guillaume Geoffroy** (IRIF) *An introduction to integrable cones as a model of linear logic*

Sémantique

Mercredi 18 octobre 2023, 10 heures 45, Salle 3052, 3ème étage du bâtiment Sophie Germain

**Pierre Clairambault** (CNRS, Université d'Aix-Marseille) *From Thin Concurrent Games to Relational Models*

Recently, there has been renewed interest in various extensions of relational models; either quantitative (e.g. the weighted relational model), or proof-relevant (e.g. distributors / generalized species of structure). In this talk, I will present recent results examining this dynamic-to-static question for such generalized relational models; in particular I will aim to arrive at a recent result obtained together with Olimpieri and Paquet: a cartesian closed pseudofunctor from the cartesian closed bicategory of thin concurrent games, to that of Fiore, Gambino, Hyland and Winskel's generalized species of structure.

Sémantique

Mercredi 4 octobre 2023, 10 heures 45, Salle 3052, 3ème étage du bâtiment Sophie Germain

**Ryan Kavanagh** (McGill University) *Stable Semantics for Recursive Session-Typed Processes*

Sémantique

Mardi 25 juillet 2023, 10 heures 30, Salle 146 (Olympe de Gouges)

**Clovis Eberhart** (National Institute of Informatics (NII, Tokyo)) *A Compositional Approach to Parity Games*

Sémantique

Mardi 21 février 2023, 10 heures 30, Salle 1007

**Nima Rasekh** (Max Planck Institute in Mathematics (MPIM) Bonn) *Category Theory of Universes*

Sémantique

Mardi 10 janvier 2023, 11 heures, Salle 1007

**Paul Ruet** (IRIF) *Asymptotic cones of groups and complexity*

#### Année 2022

Sémantique

Mardi 6 décembre 2022, 10 heures 30, Salle 1007

**Ariadne Si Suo** (University of Oxford) *Semiring Tensor and Iteration Theory*

A basic class of effects comes from the algebraic theory of modules for a semiring. The tensor of such theories is determined by the usually more tractable semiring tensor. I’ll give some examples, and then look at how the tensors work in languages with iteration. Our main contribution concerns an important class of subtheories of module theories. We observe that the subtheory tensor is also determined by the semiring tensor for several fundamental effects. I'll look at some examples of these subtheories and their tensors, and discuss how they support iteration via the underlying subsets.

This is my undergraduate summer project with Cristina Matache, Sean Moss, and Sam Staton.

Sémantique

Vendredi 25 novembre 2022, 10 heures 30, Salle 3052

**Marco Abbadini** (Université de Salerno) *A generalization of de Vries duality to closed relations between compact Hausdorff spaces*

We propose an alternative approach, where morphisms between de Vries algebras are certain relations and composition of morphisms is usual relation composition. This gives a solution to the aforementioned drawback of DeV. The usage of relations as morphisms between de Vries algebras allows us to extend De Vries duality to a duality for the larger category of compact Hausdorff spaces and closed relations, solving a problem raised by G. Bezhanishvili, D. Gabelaia, J. Harding, and M. Jibladze (2019).

I will discuss the strong connections with the literature on domain theory, in particular with the notions of R-structures, information systems and abstract bases (Smyth, Scott, Abramsky, Jung, Vickers), and with other duality theoretical results (Jung, Sünderhauf, Kegelmann, Moshier).

Sémantique

Lundi 14 novembre 2022, 14 heures, Salle 3052

**Floris Van Doorn** (Université de Paris Saclay) *Formalizing sphere eversion in Lean*

One such result is the sphere eversion project, a formalization that shows that you can turn a sphere inside out without creasing or tearing it. We prove sphere eversion as a corollary of a much deeper theorem in differential topology, the h-principle, proven by Mikhael Gromov in 1973. The h-principle (or homotopy principle) roughly states that the only obstructions to the existence of a solution to a partial differential relation come from algebraic topology, e.g. because there is some algebraic invariant that prevents any solution from existing. This project is a collaboration of Patrick Massot, Oliver Nash and me.

Sémantique

Mardi 27 septembre 2022, 10 heures 30, Salle 3052

**Rick Blute** (University of Ottawa) *Finiteness Spaces and Monoidal Topology*

In this talk, we'll briefly review some previous results which demonstrate the utility of finiteness spaces in the types of settings we are considering and then introduce monoidal topology, and finally consider possible extensions of monoidal topology via finiteness spaces. By using Ehrhard's linearization construction, we can instead consider relations on finiteness spaces which take values in a positive partially ordered semiring. In particular, we no longer require infinitary operations. This type of semiring is important in the theory of weighted automata among other places.

Sémantique

Lundi 26 septembre 2022, 14 heures, Bâtiment Sophie Germain, salle 1007

**Marek Zawadowski** (Université de Varsovie) *Polynomial and analytic functors, revisited*

I will start with some easy examples showing how these structures can be related to one another in the category Set. It turns out that polynomial functors and monads are related to Kleisli algebras, whereas analytic functors and monads are related to Eilenberg-Moore algebras for the same monad.

Then I will show that in fact this kind of structures and relations between them can be constructed in any 2-category with some mild completeness properties, whenever a lax monoidal monad sits inside it.

Sémantique

Mardi 28 juin 2022, 9 heures 30, Salle 3052

**Eigil Fjeldgren Rischel** (University of Strathclyde) *An invitation to categorical cybernetics*

Attention à l'horaire inhabituel

Sémantique

Lundi 9 mai 2022, 16 heures 30, Exposé en ligne depuis San Diego sur galene

**Chaitanya Leena Subramaniam** (University of San Diego) *The higher universal algebra of dependently typed theories*

In this talk, I will define “dependently typed algebraic theories” (DTTs), a strict subclass of GATs for which all of the universal algebra of Lawvere-Bénabou theories generalises perfectly. Happily, the GATs describing many familiar algebraic structures (such as algebraic n-categories and n-groupoids, n ≤ ∞) are DTTs. Moreover, we will see that every kind of Set-based algebraic structure defined using finite limits can be classified by (i.e. has a syntactic description in the form of) some DTT. DTTs are especially important in the context of Martin-Löf Type Theory, since they correspond to algebraic definitions admissible within this syntactic framework.

Sémantique

Mardi 3 mai 2022, 16 heures 30, Exposé en ligne depuis San Diego sur galene

**Chaitanya Leena Subramaniam** (University of San Diego) *The universal algebra of dependently typed theories*

A different approach involves replacing the simple sorts of Lawvere-Bénabou theories with dependent types, while continuing to allow only total functions, such as in Cartmell's notion of generalised algebraic theory (GAT). Indeed, many algebraic structures defined using finite limits (such as categories) have more natural descriptions by GATs than by EATs. However, much of the elegant universal algebra of Lawvere-Bénabou theories, such as their equivalent description as monads, cannot be recovered for GATs (“GATs are a bit too general”).

In this talk, I will define “dependently typed algebraic theories” (DTTs), a strict subclass of GATs for which all of the universal algebra of Lawvere-Bénabou theories generalises perfectly. Happily, the GATs describing many familiar algebraic structures (such as algebraic n-categories and n-groupoids, n ≤ ∞) are DTTs. Moreover, we will see that every kind of Set-based algebraic structure defined using finite limits can be classified by (i.e. has a syntactic description in the form of) some DTT. DTTs are especially important in the context of Martin-Löf Type Theory, since they correspond to algebraic definitions admissible within this syntactic framework.

Sémantique

Mardi 5 avril 2022, 10 heures 30, Salle 3052

**Najwa Ghannoum** (Université de Nice) *Classification of finite categories with grouplike endomorphism monoids*

Sémantique

Lundi 28 mars 2022, 11 heures, Salle 3052

**Sylvain Douteau** (Stockholm University) *Théories de l'homotopie stratifiées et équivalences de Kan-Quillen stratifiées.*

Sémantique

Lundi 28 mars 2022, 9 heures 30, Salle 3052

**Pierre-Alain Jacqmin** (Université catholique de Louvain) *Propriétés d'exactitude stables par pro-complétion*

#### Année 2021

Sémantique

Lundi 29 novembre 2021, 15 heures 30, Salle 3052

**Ivan Di Liberti** (Czech Academy of Sciences) *Context, Judgement, Deduction*

The talk is based on a joint work with Greta Coraglia: https://arxiv.org/abs/2111.09438

Sémantique

Mardi 16 novembre 2021, 10 heures 30, Salle 3052

**Nicolas Blanco** (University of Birmingham) *Four equivalent perspectives on models of LL*

First, I will recall the usual perspective as a category with extra structure to interpret the connectives, namely a *-autonomous category. Then, I will introduce polycategories where the connectives are defined through a universal properties. The equivalence between the two goes back to Cockett and Seely in 1997 although the version that I will present is slightly modified.

The third approach uses bifibred polycategories. There the connectives are interpreted by fibrational properties. This and it being equivalent to the previous perspective is new. Through some examples I will illustrate how it can be used to build more refined models from existing ones. Finally, it has been observed by Shulman that *-autonomous categories correspond to Frobenius pseudomonoid internal to the 2-polycategory of multivariable adjunctions. I will show how it is connected to the fibrational picture by a polycategorical Grothendieck correspondence.

If time permits I will discuss some subtleties concerning the aforementioned 2-polycategory that calls for a weak variant of the notion of 2-polycategory.

Quatre approches équivalentes pour les modèles de LL

Dans cet exposé je vais décrire quatre façons équivalentes d'assigner une sémantique à la logique linéaire, en me focalisant sur le fragment multiplicatif classique.

Tout d'abord, je rappellerai la perspective usuelle qui consiste à doter des catégories de structures supplémentaires pour interpréter les connecteurs, i.e. les catégories *-autonomes. Puis j'introduirai la notion de polycatégorie dans laquelle les connecteurs sont définis au travers de propriétés universelles. L'équivalence des deux notions a été démontrée par Cockett et Seely en 1997, si ce n'est que la version que je présenterai a été légèrement modifiée.

La troisième perspective utilise la notion de polycatégorie bifibrée. Les connecteurs y sont introduit au moyen de propriétés fibrationelles. Cette approche et le fait quelle est équivalente aux précédentes est nouvelle. J'illustrerai au travers d'exemples comment cela permet de définir de nouveaux modèles plus raffinés à partir de modèles existants.

Enfin, il a été observé par Shulman que les catégories *-autonomes correspondent aux pseudomonoïdes de Frobenius internes à la 2-polycatégorie des adjonctions à plusieurs variables. Je montrerai comment cela est liée à la perspective fibrationnelle au travers d'une correspondance de Grothendieck polycatégorielle.

Si le temps le permet, je discuterai plus en détails certaines subtilités à propos de cette 2-polycatégorie qui poussent à définir une version faible de la notion de 2-polycatégorie.

Sémantique

Mardi 9 novembre 2021, 10 heures 30, Exposé à distance sur Galène – salle 3052 virtuelle

**Thomas Ehrhard** (CNRS, Université de Paris) *Coherent Differentiation [Part 3]*

Sémantique

Mardi 2 novembre 2021, 10 heures 30, Exposé à distance sur Galène – salle 3052 virtuelle

**Thomas Ehrhard** (CNRS, Université de Paris) *Coherent Differentiation [Part 2]*

Sémantique

Mardi 26 octobre 2021, 10 heures 30, Exposé à distance sur Galène – salle 3052 virtuelle

**Thomas Ehrhard** (CNRS, Université de Paris) *Coherent Differentiation [Part 1]*

Sémantique

Mardi 19 octobre 2021, 10 heures 30, Salle 3052

**Théo Winterhalter** (Max Planck Institute Bochum (Allemagne)) *SSProve: A foundational framework for modular cryptographic proofs in Coq*

Sémantique

Mardi 12 octobre 2021, 10 heures 30, Exposé à distance sur Galène – salle 3052 virtuelle

**Tom Hirschowitz** (CNRS, Université Savoie Mont Blanc) *A categorical framework for congruence of applicative bisimilarity [Part Three]*

This is joint work with Ambroise Lafont.

Sémantique

Mardi 5 octobre 2021, 10 heures 30, Online talk at our Galène server: https://crocus.irif.fr:8443/group/gt-semantique

**Tom Hirschowitz** (CNRS, Université Savoie Mont Blanc) *A categorical framework for congruence of applicative bisimilarity [Part Two]*

This is joint work with Ambroise Lafont.

This is the second part of a series of two talks.

Sémantique

Mardi 21 septembre 2021, 11 heures, Online talk at our Galène server: https://crocus.irif.fr:8443/group/gt-semantique

**Tom Hirschowitz** (CNRS, Université Savoie Mont Blanc) *A categorical framework for congruence of applicative bisimilarity [Part one]*

This is joint work with Ambroise Lafont.

This is the first part of a series of two online talks. The second talk will take place on October the 5th.

Sémantique

Mardi 27 avril 2021, 10 heures, Exposé à distance sur Galène – salle 3052 virtuelle

**Soichiro Fujii** (Research Institute in Mathematical Science (RIMS), Kyoto) *Completeness and injectivity*

#### Année 2020

Sémantique

Mardi 15 décembre 2020, 11 heures 30, Exposé à distance sur Galène – https://crocus.irif.fr:8443/group/gt-semantique

**Jean-Simon Lemay** (University of Oxford (UK)) *On the coalgebras of a differential category and how to construct coderelictions from coalgebra structure.*

In this talk, we will take a look at the coalgebras of a differential category and explain how to construct coderelictions from coalgebra structure, which results in a new axiomatization of differential categories. This new axiomatization helps provide an alternative proof that free exponential modalities always come equipped with a unique codereliction, and thus every Lafont category with biproducts is a differential category. We will also explain how, under a mild limit condition, the coEilenberg-Moore category of differential category is in fact a tangent category! Tangent categories formalize the basis of differential calculus on smooth manifolds. Thus, the coalgebras of a differential category can be seen as generalized smooth manifolds, while the cofree coalgebras are interpreted as generalized Euclidean spaces.

This talk is based on and is an extension of a paper by Cockett, Lucyshyn-Wright, and Lemay: https://drops.dagstuhl.de/opus/volltexte/2020/11660/pdf/LIPIcs-CSL-2020-17.pdf

Deuxième exposé de la matinée 11:30 – 12:45

Sémantique

Mardi 15 décembre 2020, 10 heures, Exposé à distance sur Galène – https://crocus.irif.fr:8443/group/gt-semantique

**Paul Lessard** (Macquarie University) *Progress Towards a Practical Type Theory for Symmetric Monoidal Bicategories*

In this talk I will:

-) motivate Shulman’s PTT and provide an introduction to that theory; and

-) describe progress towards a similar type theory for symmetric monoidal bi-categories.

In particular, in this second part:

+) I will compare the role played by nice presentations, PROPs, and signatures in the semantics of PTT to the role played by (generalized) 2- and 3-computads for (the globular operad for) quasi-strict symmetric monoidal bi-categories; and

+) introduce the basic judgements of our proposed syntax - along with their ‘sets with elements’ style interpretation

You will find more on Paul Lessard's work here: https://sites.google.com/view/paul-roy-lessard

Premier exposé de la matinée 10:00 – 11:15

Sémantique

Mardi 3 mars 2020, 10 heures 30, Salle 4033

**Pierre Cagne** (Université de Bergen (Norvège)) *The symmetries of spheres in univalent foundations*

Attention au changement de salle 4033 au lieu de la salle 3014 habituelle

Sémantique

Mardi 28 janvier 2020, 10 heures 30, Salle 3052

**Antti Kuusisto** (University of Helsinki) *A Turing-complete extension of first-order logic*

Sémantique

Mercredi 22 janvier 2020, 10 heures 30, Salle 3014

**John Bourke** (Masaryk University (Brno)) *Weak adjoint functor theorems and accessible infinity-cosmoi*

Sémantique

Mardi 7 janvier 2020, 11 heures, Salle 3052

**Robin Piedeleu** (University College London) *Une approche graphique des systèmes concurrents*

Il s'agit de travaux en collaboration avec Filippo Bonchi, Pawel Sobocinski et Fabio Zanasi.

GdT joint au groupe de travail ACS

#### Année 2019

Sémantique

Mardi 17 décembre 2019, 10 heures 30, Salle 3052

**Yannick Zakowski** (Irisa/Inria) *From representing recursive and impure programs in Coq to a modular formal semantics of LLVM IR*

In this talk, we will focus on the design and implementation of Interaction Trees (ITrees), a general-purpose data-structure for representing in Coq potentially divergent, effectful, programs. ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from event handlers, which give meaning to events by defining their semantics as monadic actions. They are expressive enough to represent impure and potentially nonterminating, mutually recursive computations in Coq. Finally, they give rise to a theory enabling equational reasoning, up to weak bisimulation, about ITrees and monadic computations built from them. In contrast to other approaches, ITrees are executable via code extraction.

ITrees are expressive enough to serve as a language of specification for most projects of the DeepSpec ecosystem, making them a sort of 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 a second part of this talk, we will focus on how ITrees are used in one of the DeepSpec projects in particular: Vellvm. More specifically, we will give an account of the ongoing effort to use ITrees as a mean to define a modular formal semantics of LLVM IR.

Sémantique

Mardi 3 décembre 2019, 11 heures 15, Salle 3052

**Ivan Di Liberti** (Masaryk University (Brno)) *Topos theoretic approaches to formal model theory*

Sémantique

Mardi 3 décembre 2019, 10 heures, Salle 3052

**Valentin Blot** (INRIA, ENS Paris-Saclay) *Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types*

Sémantique

Mardi 26 novembre 2019, 10 heures 30, Salle 3014

**Vladimir Zamdzhiev** (Tulane University) *Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory*

Sémantique

Mardi 19 novembre 2019, 10 heures 30, Salle 3052

**Fredrik Dahlqvist** (University College London) *A probabilistic approach to floating point arithmetic*

Given an input distribution, the model requires the distribution of rounding errors. We show how to exactly compute this distribution for low precision arithmetic. For high precision arithmetic we derive a simple but surprisingly useful approximation. The model is then entirely compositional: given a numerical program written in a simple imperative programing language we can recursively compute the distribution of rounding errors at each step and propagate it through each program instruction. This is done by applying a formalism originaly developed by Kozen to understand the semantics of probabilistic programs, for example how probability distributions gets transformed by assignments or “if then else” statements.

Sémantique

Mardi 8 octobre 2019, 10 heures 30, Salle 3052

**Clovis Eberhart** (National Institute of Informatics, Tokyo) *History-Dependent Nominal μ-Calculus*

Sémantique

Mardi 2 juillet 2019, 14 heures, Salle 3052

**Henning Basold** (Leiden University) *Guarded Recursion for Probabilistic Programming and Probabilistic Logic*

In this talk, I will first show how a fibration can be extended, under mild conditions, to a fibration with guarded recursion. The abstract settings of fibrations allows the application of guarded recursion in various settings such as probabilistic programming and reasoning. We will see this in the second part of the talk in action, where we will devise a language for coinductive probabilistic processes based on guarded recursion that retains termination. The semantics of this language is obtained by applying the construction from the first part of the talk to quasi-Borel spaces. This gives an alternative language with guaranteed termination to the probabilistic language with unrestricted recursion recently given by Vákár et al. (POPL'19).

Sémantique

Mardi 2 avril 2019, 10 heures 30, Salle 3052

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

Sémantique

Lundi 18 mars 2019, 14 heures, Salle 3052

**Michel Schellekens** (University College Cork) *Expedient Algebra: Duality and Entropy Conservation*

We show that EXP-computations, made reversible through history-keeping, act as closed systems in which entropy is conserved. Thus modularity of timing is linked to entropy conservation of data flow, sharpening traditional entropy preservation guaranteed by the second law of thermodynamics for reversible systems. This type of conservation typically holds for the case of energy, but not for entropy. A salient point is that for algorithms satisfying distribution control, entropy is neither created nor destroyed, merely transferred from one form, i.e. quantitative entropy, to another, i.e. positional entropy.

We establish the Entropy Conservation Laws ECL-1 and ECL-2. ECL-1 expresses the inverse proportionality of positional and quantitative entropy for distributions over series-parallel orders and their duals. ECL-2, a computational version of entropy conservation, expresses that order established by the expedient product (with history) on labels is proportionally destroyed on indices by a shadow transformation in the dual space. The laws shed new light on the properties of algorithms for which distribution control, and hence modular timing, is guaranteed.

Sémantique

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

**Eric Finster** (INRIA) *L'algèbre universelle supérieur dans la théorie des types dependants*

Sémantique

Vendredi 1 février 2019, 10 heures 30, Salle 3052

**Nobuko Yoshida** (Imperial College London) *Behavioural Type-Based Static Verification Framework for Go*

POPL'17 Fencing off go: liveness and safety for channel-based programming ICSE'18 A Static Verification Framework for Message Passing in Go using Behavioural Types POPL'19 Distributed Programming Using Role Parametric Session Types in Go.

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks. We present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioral types, where the types are model checked for liveness and safety. We also present a recent code generation for Go.

Sémantique

Mardi 29 janvier 2019, 11 heures, Salle 3052

**Giulio Guerrieri** (Università di Bologna) *Types by Need (joint work with Beniamino Accattoli and Maico Leberle)*

Sémantique

Lundi 28 janvier 2019, 11 heures, Salle 3052

**Fredrik Dahlqvist** (UCL - Department of Computer Science) *Semantics of higher-order probabilistic programs with conditioning*

Sémantique

Mardi 8 janvier 2019, 10 heures 30, Salle 3052

**Jean Bénabou** *Les multiples facettes de la « construction de Grothendieck »*

#### Année 2018

Sémantique

Mardi 4 décembre 2018, 11 heures 20, Amphi Turing, Bâtiment Sophie Germain

**Eric Degiuli** (ENS) *Random Language Model: a path to principled complexity*

Sémantique

Lundi 26 novembre 2018, 10 heures 45, Salle 3052

**Hendrik Maarand** (Tallinn University of Technology) *Derivatives of Existentially Regular Trace Languages*

Sémantique

Mardi 6 novembre 2018, 10 heures 30, Salle 3052

**Rick Blute** (University of Ottawa) *Finiteness spaces and generalized power series*

In the present work, we take morphisms to be partial functions preserving the finitary structure rather than relations. The resulting category is symmetric monoidal closed, complete and cocomplete. Any pair of an internal monoid in this category and a ring induces a ring of generalized power series by an extension of the Ribenboim construction based on Ehrhard’s notion of linearization of a finiteness space. We thus further generalize Ribenboim’s constructions. We give several examples of rings which arise from this construction, including the ring of Puiseux series and the ring of formal power series generated by a free monoid. This is joint work with Cockett, Jacqmin and Scott.

We'll also present some results of Beauvais-Fiesthauer, Dewan and Drummond on the embedding of topological spaces into finiteness spaces and discuss how this might be of use in the analysis of etale groupoids and their C*-algebras.

Sémantique

Mardi 16 octobre 2018, 10 heures 30, Salle 3052

**Thomas Ehrhard** (IRIF) *Une remarque sur les espaces cohérents probabilistes et la distance opérationnelle entre les programmes*

Sémantique

Mardi 18 septembre 2018, 10 heures, Salle 3052

**Paul-André Mellies** (IRIF) *Template games: a model of differential linear logic*

Sémantique

Mardi 18 septembre 2018, 11 heures, Salle 3052

**Jean-Simon Lemay** (University of Oxford) *Differential Categories Revisited*

Les catégories différentielles ont été introduites afin de fournir une sémantique catégorique minime pour la logique linéaire différentielle. Cependant, il existe trois approches d'axiomatiser la dérivée par les “deriving transformations”, “coderelictions”, “creation maps” - considérés pendant longtemps comme des notions distinctes. Récemment, avec Blute, Cockett et Seely, nous avons revisité les axiomes d’une catégorie différentielle et démontré que pour les modèles catégoriques de logique linéaire différentielle, les trois approches sont équivalentes. Il y a donc qu’une seule notion de différentielle.

Sémantique

Mardi 15 mai 2018, 11 heures, Salle 3052

**Tarmo Uustalu** (Reykjavik University and Tallinn University of Technology) *Nested and labelled sequent calculi for bi-intuitionistic propositional logic*

This is joint work with Luís Pinto (Universidade do Minho).

Sémantique

Mardi 20 février 2018, 11 heures, Salle 3052

**Shin-Ya Katsumata** (National Institute of Informatics, Tokyo) *Codensity liftings of monads*

(Joint work with Tetsuya Sato; presented in CALCO 2015)

Sémantique

Mercredi 17 janvier 2018, 10 heures, Salle 3052

**Luc Pellissier** (ENS Lyon) *Intersection Types, Linear Approximations and the Grothendieck construction*

Based on a joint work with Damiano Mazza and Pierre Vial.

Sémantique

Mercredi 17 janvier 2018, 11 heures, Salle 3052

**Soichiro Fujii** (National Institute of Informatics (NII, Tokyo)) *A unified framework for notions of algebraic theory*

First I will explain how each notion of algebraic theory can be identified with a certain monoidal category, in such a way that theories correspond to monoids. Then I will introduce a categorical structure underlying the definition of models of theories. In specific examples, it often arises in the form of oplax action or enrichment. Finally I will uniformly characterize categories of models for various notions of algebraic theory, by a double-categorical universal property in the pseudo-double category of profunctors.

#### Année 2017

Sémantique

Mardi 5 décembre 2017, 10 heures 30, Salle 3052

**Kenji Maillard** (INRIA et ENS) *F* : Dijkstra-monads at work*

Sémantique

Mercredi 29 novembre 2017, 10 heures 30, Salle 3052

**Simona Paoli** (University of Leicester) *n-Fold models of weak n-categories*

Sémantique

Mardi 21 novembre 2017, 10 heures 30, Salle 3052

**John Baez** (UCLA Riverside) *Compositionality in Network Theory*

Sémantique

Mardi 7 novembre 2017, 10 heures 30, Salle 3052

**Tobias Heindel** (Université de Leipzig) *Formal language theory beyond trees and forests*

Sémantique

Mardi 31 octobre 2017, 10 heures 30, Salle 3052

**Nicolas Behr** (IRIF) *Combinatorial Hopf algebras and rewriting: the rule algebra framework*

Sémantique

Jeudi 31 août 2017, 14 heures, Salle 3052

**Zoran Petric** (Mathematical Institute, Academy of Sciences, Belgrade) *Frobenius spheres*

The talk is based on the paper “Spheres as Frobenius objects”, co-authored with Djordje Baralic and Sonja Telebakovic, which is available at arxiv.

Sémantique

Mardi 18 juillet 2017, 14 heures, Salle 3052

**Noam Zeilberger** (University of Birmingham) *Some bridges between lambda calculus and graphs on surfaces*

Sémantique

Vendredi 30 juin 2017, 16 heures 30, Salle 3052

**Niccolò Veltri** (Laboratory of Software Science, Tallinn) *Partiality and container monads*

Sémantique

Mardi 13 juin 2017, 11 heures, Salle 2012

**Elaine Pimentel** (Universidade Federal do Rio Grande do Norte (Brasil)) *A uniform framework for substructural logics with modalities*

This is a joint work with Carlos Olarte and Björn Lellmann

ATTENTION A LA SALLE INHABITUELLE (2012 Sophie Germain)

Sémantique

Mardi 28 février 2017, 11 heures, Salle 3052

**Ran Chen** (Inria) *Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm*

We present a human readable and rather intuitive formal proof for the classical Tarjan-1972 algorithms for finding strongly connected components in directed graphs. Tarjan’s algorithm consists in an efficient one-pass depth-first search traversal in graphs which traces the bases of strongly connected components. We describe the algorithm in a functional programming style with abstract values for vertices in graphs, with functions between vertices and their successors, and with data types such that lists (for representing immutable stacks) and sets. We use the Why3 system and the Why3-logic to express these proofs and fully check them by computer.

Sémantique

Mardi 24 janvier 2017, 11 heures, Salle 3052

**Arnaud Spiwack** (Tweag I/O) *Retrofitting linear types*

I had always had the belief that to add linear types to a language was a rather intrusive procedure and that a language with linear types would basically be an entirely new language. The Rust language is a case in point: it has a linear-like type system, but it's a very different language from your run-of-the-mill functional language.

This turns out not to be the case: this talk presents a way to extend a functional programming language. We are targeting Haskell but there is little specific to Haskell in this presentation. I will focus mostly on the type system and how it can be generalised: among other things the type system extends to dependent types.

Sémantique

Vendredi 13 janvier 2017, 14 heures, Salle 3052

**Tarmo Uustalu** (Tallinn University of Technology) *Interaction morphisms*

Tarmo Uustalu, Tallinn U of Technology

I will propose interaction morphisms as a means to specify how an effectful computation is to be run, provided a state in a context. An interaction morphism of a monad T and a comonad D is a family of maps T X x D Y → X x Y natural in X and Y and subject to some equations. Interaction morphisms turn out to be a natural concept with a number of neat properties. In particular, interaction morphisms are the same as monoids in a certain monoidal category; interaction morphisms of T and D are in a bijective correspondence with carrier-preserving functors between the categories of coalgebras of D and stateful runners of T (monad morphisms from T to state monads); they are also in a bijective correspondence with monad morphisms from T to a monad induced in a certain way by D.

This is joint work with Shin-ya Katsumata (University of Kyoto).

Sémantique

Mardi 10 janvier 2017, 11 heures, Salle 3052

**Fanny He** (Université de Bath, UK) *The atomic lambda-mu-calculus*

One approach for the former is to gain more control over duplication and deletion of terms, by introducing sharings of common subterms inside a lambda-term, similarly to optimal reduction graphs. This has been done by Gundersen, Heijltjes and Parigot, via the atomic lambda-calculus, a calculus extending the lambda-calculus with explicit sharings, and allowing duplications on individual constructors. It enjoys full-laziness, avoiding unnecessary duplications of constant expressions.

For the latter, an extension of the lambda-calculus linking classical formulas to control flow constructs via Curry-Howard correspondence, the lambda-mu-calculus, was developed by Parigot. New operators in the lambda-mu-calculus correspond to continuations, representing the remaining work in a program.

Can we combine sharing with control operators and thus obtain another extension of the lambda-calculus satisfying full-laziness and featuring control operators? A first challenge is to combine explicit sharings or substitutions with mu-reduction and substitution, and we introduce a right-associative application as in Saurin-Gaboardi's lambda-mu-calculus with streams to overcome this challenge. Another difficulty is to adapt the type system for lambda-mu with multiple conclusions, distinguishing one main conclusion (with a meta-disjunction connective), to a type system in which each rule can be applied to atoms (which corresponds to duplications on individual term constructors), and where no distinction is made between object and meta-level. I will present how to combine these two type systems in the simplest possible way.

I will present the atomic lambda-mu-calculus, which aims to naturally extend the two calculi presented above, giving the simplest type system combining and preserving their properties.

#### Année 2016

Sémantique

Mercredi 21 décembre 2016, 11 heures, Salle 3052

**Victoria Lebed** (Trinity College, Dublin) *Que savent les tresses sur les tableaux de Young ?*

Sémantique

Mardi 20 décembre 2016, 11 heures, Salle 3052

**Clovis Eberhart** (LAMA, Chambéry) *Séquences justifiées et diagrammes de cordes : deux approches de la sémantique de jeux concurrents*

Sémantique

Mardi 6 décembre 2016, 11 heures, Salle 3052

**Yann Régis-Gianas** (IRIF) *Explaining Program Differences Using Oracles*

We present a formal framework to characterize differences between deterministic programs in terms of their small-step semantics. This language-agnostic framework defines the notion of /difference languages/ in which /oracles/—programs that relate small-step executions of pairs of program written in a same language—can be written, reasoned about and composed.

We illustrate this framework by instantiating it on a toy imperative language and by presenting several /difference languages/ ranging from trivial equivalence-preserving syntactic transformations to characterized semantic differences. Through those examples, we will present the basis of our framework, show how to use it to relate syntactic changes with their effect on semantics, how one can abstract away from the small-step semantics presentation, and discuss the composability of oracles.

This is joint work with Thibaut Girka (IRIF - MERCE) and David Mentré (MERCE)

Sémantique

Mardi 15 novembre 2016, 11 heures, Salle 3052

**José Espírito Santo** (University of Minho) *Call-by-name, call-by-value and intuitionistic logic*

Sémantique

Mardi 8 novembre 2016, 11 heures, Salle 3052

**Gustavo Petri** (IRIF) *Safe and Scalable Cloud Programming*

Sémantique

Mardi 18 octobre 2016, 10 heures 30, Salle 3052

**Pablo Barenbaum** (Université de Buenos Aires - CONICET) *Finite Family Developments for the Linear Substitution Calculus*

Joint work with Eduardo Bonelli.

Sémantique

Mardi 18 octobre 2016, 11 heures 30, Salle 3052

**Masahito Hasegawa** (Research Institute in Mathematical Sciences (RIMS)) *Traced star-autonomous categories are compact closed*

We also discuss what would happen if we remove symmetry, thus the following question: is there a non-symmetric star-autonomous category with a (suitably generalized) trace which is not pivotal? Our recent attempt suggests that the answer is again no, but the situation is much subtler than the symmetric case.

The result on the symmetric case is a joint work with Tamas Hajgato.

Sémantique

Mardi 5 juillet 2016, 11 heures, Salle 3052

**Shane Mansfield** (IRIF) *Empirical Models and Contextuality*

Sémantique

Mardi 7 juin 2016, 11 heures, Salle 3052

**Thomas Leventis** (I2M Marseille) *Probabilistic lambda-theories*

In this talk we will recover this notion of presentation through equalities in the probabilistic lambda-calculus. We will show how some usual notions can be translated in the probabilistic world. In particular we will define a notion of probabilistic Böhm tree, and show a separability result. This will implies that just like in the deterministic setting the Böhm tree equality is the same as the observational equivalence.

Attention, mardi 7 double séance

Sémantique

Mardi 7 juin 2016, 10 heures, Salle 3052

**Antoine Allioux** (IRIF) *Krivine machine and Taylor expansion in a non-uniform setting*

We generalize this resource-driven Krivine machine to the case of the algebraic $\lambda$-calculus. The latter is an extension of the pure $\lambda$-calculus allowing for the linear combination of $\lambda$-terms with coefficients taken from a semiring. Our machine associates a $\lambda$-term $M$ and a resource annotation $t$ with a scalar $\alpha$ in the semiring describing some quantitative properties of the linear head reduction of $M$.

In the particular case of non-negative real numbers and of algebraic terms $M$ representing probability distributions, the coefficient $\alpha$ gives the probability that the linear head reduction actually uses exactly the resources annotated by $t$. In the general case, we prove that the coefficient $\alpha$ can be recovered from the coefficient of $t$ in the Taylor expansion of $M$ and from the normal form of $t$.

Attention, mardi 7 double séance !

Sémantique

Mardi 17 mai 2016, 11 heures, Salle 3052

**Daniel Leivant** (Indiana University Bloomington) *Syntax directed coproofs for Propositional Dynamic Logic*

Contrary to proofs, which are generated inductively top-down, coproofs are generated coinductively bottom-up, and may have infinite branches. However, our inference rules allow this only via state-changes, and as a result are sound.

We also prove the semantic completeness of our formalism, and apply it to obtain new interpolation theorems for PDL.

Sémantique

Jeudi 7 avril 2016, 16 heures, Salle 3052

**Flavien Breuvart** (INRIA Focus (Université de Bologna, IT)) *L'encodage probabiliste: vers une formalisation systématique des langages probabilistes, déterministiques et potentiellement divergents.*

Attention au jour et horaire inhabituels !

Sémantique

Mardi 29 mars 2016, 10 heures 30, Salle 3052

**Andrew Polonsky** (IRIF) *Interpreting infinite terms*

\f.f(Ω), \f.f^2(Ω), \f.f^3(Ω), …, \f.f^n(Ω), ….

The infinite term \f.f(f(f…)) is the limit of the above sequence, and in the infinitary lambda calculus all fpcs reduce to this term, which is an infinitary normal form. It would seem natural to extend the interpretation function to cover infinitary terms as well, however, naive attempts to do this fail. The problem is already present in the first-order case: finite terms over a signature ∑ can be interpreted by means of the initial semantics – where the free algebra of terms admits a canonical homomorphism to any other ∑-algebra. However, the infinite terms are elements of the cofinal coalgebra, which universal property concerns maps INTO the algebra, rather than out of it. We are thus faced with a “koan”:

- What does it mean to interpret infinite terms?*

While we shall not provide a (co)final solution to this koan, we will offer germs of some possible approaches, with the hope of starting a discussion that could follow this short talk.

Attention à l'horaire inhabituelle