In this talk we recall how quantum operations (also known as channels) are modelled mathematically in both the Heisenberg and Schrödinger pictures of quantum theory. The two pictures are dual to each other and we recall how the theory of operator spaces can be used to describe this duality in mathematical terms. Operator spaces, studied in noncommutative geometry, are the noncommutative (or quantum) analogue of Banach spaces. We prove that the category OS (operator spaces with complete contractions as morphisms) is locally countably presentable and a model of Intuitionistic Linear Logic in the sense of Lafont. We then describe a model of Classical Linear Logic, based on OS, whose duality is compatible with the Heisenberg-Schrödinger duality of quantum theory. In the later model, the mathematical descriptions of systems in the Heisenberg picture correspond to formulas with negative logical polarity, whereas those in the Schrödinger picture correspond to formulas with positive logical polarity. Time permitting, we can also cover other interesting features of the model(s). Joint work with Bert Lindenhovius.

Effectful streams give formal compositional coinductive semantics to effectful synchronous dataflow programs. Effectful streams allow us to develop notions of trace and bisimulation for effectful Mealy machines; bisimilarity implies effectful trace equivalence. This talk is based on joint work with Giovanni de Felice and Mario Román, and on more recent joint work with Filippo Bonchi and Mario Román.

I will try to convince you type checkers can be seen as logic programs with ‘directions’, and doing type checking correspond to proof reductions in classical linear logic. This gives us implementations of type checking algorithms for free, by writing bidirectional typing rules as directional logic programs. If time permits, I will tell you some categorical details, or possible extensions to accommodate more expressive type systems. Based on joint work with Vikraman Choudhury and Neel Krishnaswami.

Noticing the similarity between the monotone weak distributive laws combining two layers of non-determinism in sets and in compact Hausdorff spaces, we study whether the latter law can be obtained automatically as a weak lifting of the former. This holds partially, but does not generalize to other categories of algebras: we then characterize when exactly monotone weak distributive laws over powerset monads in categories of algebras exist, exhibiting a law combining probabilities and non-determinism in compact Hausdorff spaces and showing on the other hand that such laws do not exist in a lot of other cases.

In this talk I will introduce arrow algebras, “algebraic” structures inducing toposes through Pitts' tripos-to-topos construction which generalise Alexandre Miquel’s implicative algebras, and I will present appropriate notions of morphisms between arrow algebras corresponding to morphisms of the associated triposes. The weakening of the axioms, from implicative algebras to arrow algebras, allows the latter to perfectly factor through the construction of realizability toposes starting from partial combinatory algebras; moreover, it allows for a particularly simple description of subtoposes of the induced toposes in terms of nuclei on the underlying arrow algebra, generalising the notion of nucleus on a frame. As an example of these properties, I will show how modified realizability can be lifted to the level of arrow algebras, recovering and extending some results known in the literature at the level of partial combinatory algebras.

A clone on a set is a family of finitary operations on the set that is closed under projections and composition. Abstract clones are the algebras for the many-sorted equational presentation that axiomatises this structure. Categorically, they are (finitary, one-sorted) algebraic theories. Inspired by works in algebraic logic, we shall define an equational class of abstract clones, tentatively dubbed “partition clones'', and describe some of their properties; in particular, we will show that this family of abstract clones has lot in common with Boolean algebras. Among the results we shall present, there is a theorem concerning the lattice of hypervarieties (i.e. varieties of abstract clones) already proven in 1991 by George M. Bergman from a different perspective. We shall explain the link between his approach and ours.

Proof-nets are a major contribution from linear logic. Contrary to the usual representation of proofs as derivation trees in sequent calculus, proof-nets represent proofs as general graphs respecting some correctness criterion. A standard result is that these two syntaxes correspond to each other, which is called sequentialization. Despite being a well-known theorem, its proofs in the literature are generally complex. I will present a new simple proof for proof-nets of multiplicative linear logic, modular enough to still apply in the presence of the mix-rule. Then, I will develop links between sequentialization and more general graph theory, following on works from Rétoré and Nguyễn but focusing on edge-colored graphs instead of perfect matchings.

[Joint work with Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair]

Probabilistic coherence spaces (PCSs) provide an adequate, and actually fully abstract, denotational model of probabilistic PCF (an idealised Turing complete functional language extended with probabilistic choice). Given a closed probabilistic PCF term M of type bool for instance, PCSs provide therefore a way to approximate from below the probability p that M reduces, eg, to true. I will show how, extending PCSs with an “extensional structure”, it is also possible to approximate this probability p from above. These extensional PCSs form a model of LL, and are a probabilistic analog of Berry's bidomains. I will explain how this approximation mechanism can be straightforwardly implemented using a Krivine Machine which computes finite approximants of a powerseries associated with M by the extensional PCS semantics. If time permits, there will be a demo.

In recent years, there has been much work done in probabilistic semantics. Most of them fall in one of two categories; those based on monads and those based on linear logic. At the semantic level, these two different semantics correspond to distinct basic programming abstractions. In this case, semantically, programming with monads corresponds to programming with Markov kernels, while linear logic corresponds to programming with linear operators.

In this talk I will go over recent work of mine that tries to establish a formal connection between these two families of semantics. I will start by presenting a new core calculus for programming with Markov kernels and linear operators, will show that this formalism encompasses useful models from the probabilistic semantics literature and will conclude by sketching some applications of this formalism to the new research program of synthetic probability theory.

In this presentation, we explore the foundational elements required to interpret reversible programming within a categorical framework. We use the symmetric pattern-matching language introduced by Sabry, Valiron, and Vizzotto as a reference point, and we incorporate several improvements. We show that inductive data types and recursion can also be effectively modelled in this setting. However, these results do not straightforwardly extend to the pure quantum case. We provide insights into the challenges encountered and propose potential directions for addressing these limitations, for example with guarded recursion.

(Self) references: Classical reversible semantics: https://doi.org/10.4230/LIPIcs.FSCD.2024.19 / https://arxiv.org/abs/2309.12151 First-order quantum semantics (chapter 3): https://theses.hal.science/tel-04625771 / https://arxiv.org/abs/2406.07216 Non-cartesian guarded recursion: https://arxiv.org/abs/2409.14591

Like time in physics, computations can be reversible: the inverse of a deterministic computation is itself a valid computation, provided the program's state retains sufficient information to allow rollback. However, reversing a computation in distributed systems presents a challenge due to non-determinism. The inversion process must respect causality to maintain consistency. Syntactically, reversing a concurrent program requires tracking computation events in a way that preserves information during reductions, despite the absence of a global scheduler. From a denotational perspective, traditional models interpret concurrent programs as partial orders of configurations, where configurations consist of sets of computation events. Executing a computation involves removing the corresponding events from all configurations using set difference, while discarding incompatible configurations. In this talk, we introduce a generalization of these traditional models to accommodate reversibility, employing symmetric difference. This approach interprets reversible computation as a partial group action on sets of configurations.

The Ahlbrandt-Ziegler result in model theory asserts that a countably categorical theory is characterised, up to bi-interpretability, by the topological automorphism group of its (unique) countable model, thus permitting a study of these theories by group-theoretic properties.

Removing the countable categoricity assumption necessitates using topological groupoids rather than groups. We will describe a groupoidal generalisation of the Ahlbrandt-Ziegler result using topos theory.

Our result extends the results in the topos-theoretic literature of Awodey, Butz, Caramello, Forssell and Moerdijk, while being orthogonal to the parallel generalisation of Ben Yaacov.

Summary: The starting point of this talk is the structure of the object $!Bool$ in probabilistic coherent spaces. For the purpose of building a semantics interpretation for PCF_proba, it is enough to consider elements of $!Bool$ that are promotions of elements in Bool, but $!Bool$ contains also more exotic elements, that can nonetheless be seen as probabilistic samplers (in the sense that they can handle any number of query from a program !Bool → sigma to its argument, seen as a random oracle). In this work, we present a caracterisation of all total elements in !Bool: we show that they can all be seen as *continuous mixture* of promotions. The central element of this proof is an extension to the category of integrable cones of the categorical version[1] of the De Finetti theorem (that says that there is a one-to-one correspondance between the continuous probability distributions on [0,1], and the infinite exchangeable sequence of discrete random variables on booleans).

[1] B. Jacobs and S. Staton. De finetti’s construction as a categorical limit, CMCS 2020.

Storage modalities provide the categorical interpretation of the exponential modality from Linear Logic, while differential storage modalities do the same in Differential Linear Logic. Briefly, a storage modality is a special kind of comonad, while a differential storage modality is a storage modality equipped with a deriving transformation (equivalent a codereclition). In this talk, I’ll explain how using Kelly's notion of algebraically-free commutative monoids, we can construct free differential storage modalities over storage modalities. When taking the initial storage modality, we get the initial differential storage modality which is related to the Faà di Bruno construction and also recaptures the exponential modality in Clift and Murfet's Differential Linear Logic model. This is joint work with Richard Garner.

The famous asynchronous computability theorem (ACT) relates the existence of an asynchronous wait-free shared memory protocol for solving a task with the existence of a simplicial map from a subdivision of the simplicial complex representing the inputs to the simplicial complex representing the allowable outputs. The original theorem relies on a correspondence between protocols and simplicial maps in round-structured models of computation that induce a compact topology. This correspondence, however, is far from obvious for computation models that induce a non-compact topology, and indeed previous attempts to extend the ACT have failed. This paper shows that in every non-compact model, protocols solving tasks correspond to simplicial maps that need to be continuous. It first proves a generalized ACT for sub-IIS models, some of which are non-compact, and applies it to the set agreement task. Then it proves that in general models too, protocols are simplicial maps that need to be continuous, hence showing that the topological approach is universal. Finally, it shows that the approach used in ACT that equates protocols and simplicial complexes actually works for every compact model. Our study combines, for the first time, combinatorial and point-set topological aspects of the executions admitted by the computation model.

Joint work with Hagit Attiya and Armando Castañeda.

Lawvere’s (hyper-)doctrines are a categorical tool that allows the analysis of both the syntax and the semantics of logical theories using the same mathematical structure. In this talk, we explore a possible interpretation of Henkin’s Theorem for first-order logic (“Every consistent theory has a model”) via bounded implicational existential doctrines. To achieve this goal, at first we study the meaning in the framework of doctrines of “adding a constant to a language” and “adding an axiom to a theory”. Then, starting from a consistent doctrine, we use these construction to build a rich doctrine - in which every valid formula of the kind ∃xφ(x) there exists a witness constant c such that φ© holds. Finally, we show that a rich doctrine admits a model, i.e. a morphism towards the subset doctrine. Henkin’s Theorem for doctrines follows from these results, and our proof is modelled on the main lines of the original one.

We will present a very general syntax that aims to export tools and techniques found in linear logic (intersection types, Taylor and Böhm approximations, geometry of interaction…) in a systematic way in other languages or calculus. That being still a work in progress, details will be given in a restriction of this syntax, in which we present an axiomatic definition of “approximation system”, based on a notion of fibration, aiming to capture this phenomenon as generally as possible. In this talk, we will explore the immediate consequences of the definition, introduce several concrete instances of it, and obtain well-known theorems as direct applications of the general framework.

In this talk, I will report on progress developing a fuzzy type theory, a project that started as part of the ACT 2022 Adjoint School. The motivation is to develop a logic which can model opinions, and we do this by generalizing Martin-Löf type theory. Martin-Löf type theory provides a system in which one can construct a proof (aka a term) of a proposition (aka a type), and we usually interpret such a term as saying that the proposition holds. Fuzzy type theory is a similar system in which one can provide or construct evidence (aka a fuzzy term) to support an opinion (aka a type), but the evidence (fuzzy term) comes with a parameter, for instance a real number between 0 and 1, which expresses to what extent the opinion holds. Martin-Löf type theory is closely related to category theory: from such a type system one can construct a category in which (very roughly) the types become objects and the terms become morphisms, and this can be made part of an equivalence. Thus, we base our development of fuzzy type theory to be the thing which corresponds to categories enriched in a category of fuzzy sets in the same way that Martin-Löf type theory corresponds to categories (enriched in sets).

This is joint work with Shreya Arya, Greta Coraglia, Sean O’Connor, Ana Tenório, and Hans Riess.

9:30 - 10:20 Ugo Dal Lago, Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories 10:20 - 10:40 Coffee break 10:45 Semantics working group or (= & of LL) free discussion

This talk starts with a result in classical Finite Automata Theory: 'Two regular languages with the same number of words for each length can be mapped one onto the other by a letter-to-letter (finite) transducer'.

The notion of generating function of regular languages leads to the introduction of the model of weighted automata. The conjugacy of weighted automata, a concept borrowed to symbolic dynamics, is then defined and it is shown how the above statement can be derived from the central result of this work: 'Two equivalent weighted automata are conjugate to a third onewhen the weight semiring is B, N, Z, or any Euclidean domain (and thus any (skew) field)'.

This talk is based on a joint work with Marie-Pierre Béal and Sylvain Lombardy.

10:00 - 10:50 Claudia Faggian, Higher Order Bayesian Networks, Exactly 10:50 - 11:10 Coffee break 11:10 - 12:00 Fredrik Dahlqvist, Sampling semantics for probabilistic programs 12:00 - 14:00 Lunch break 14:00 - 14:50 Pedro Azevedo de Amorim, Compositional Expected Cost Semantics for Functional Probabilistic Programs 14:50 - 15:40 Paul-André Melliès, Asynchronous template games and strategies 15:40 - 16:00 Coffee break 16:00 - 16:50 Guillaume Baudart, Schedule Agnostic Semantics for Reactive Probabilistic Programming 16:50 - 17:40 Thomas Ehrhard, A syntax for coherent differentiation

This will be an introductory talk about geometric methods in fault-tolerant distributed computing. More specifically, my main goal will be to state, and give a proof sketch, of the Asynchronous Computability Theorem of Herlihy and Shavit (1993). This theorem shows that a computational question (can a given protocol solve a distributed task?) can be reduced to a geometric question (“is there a simplicial map between some simplicial complexes?”). This approach has been particularly successful to establish impossibility results in distributed computing. While the original theorem of Herlihy and Shavit was formulated in the specific setting of wait-free processes communicating via shared read/write registers, it it in fact applicable to a much wider class of computational models, and I will try to convey that generality.

Team Semantics generalizes the usual Tarski semantics for first-order logic by interpreting formulas via sets of assignments rather than single assignments. This results in several extensions of first-order logic, such as dependence, inclusion, and independence logic, whose expressive power corresponds to different fragments of existential second order logic. In this talk I will describe how, despite this high expressive power, these logics lend themselves quite well to a model-theoretic investigation. In particular, I will introduce a category of models and higher-order maps for structures in team semantics, and I will try to relate it to the framework of AECats (accessible categories with monomorphisms and suitable colimits) introduced by Kirby.

Ehrhard and Regnier's Taylor expansion provides an approximation of λ-terms by vectors of multilinear « resource » λ-terms, and it commutes with normalisation towards Böhm trees. This can be seen as a consequence of the simulation property enjoyed by the extension of the Taylor approximation to the 001-infinitary λ-calculus, as shown in [C. and Vaux Auclair, to appear]. The published version of this extension is only qualitative (the coefficients of the vectors are booleans), but ongoing resarch suggests a quantitative counterpart by reformulating Ehrahrd and Regnier's uniformity arguments. This advocates for considering the 001-infinitary λ-calculus as a “natural” setting for defining th Taylor approximation; a limitation to this statement is that a conservativity property is lost when going infinitary. In addition, adapting our work to 101-infinitary λ-terms suggests a resource λ-calculus approximating the lazy λ-calculus.

This talk concerns a category-theoretical construction of linear exponential comonad in terms of measure theoretical transition kernels.

(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.

Denotational models can roughly be classified in two kinds: static models (domains, relations, coherence spaces, etc), which record atemporal final “states” of completed executions; and dynamic models (game semantics, GoI, etc), which additionally describe how such final states are reached with temporal or causal information. The link between the two seems intuitively simple as it suffices to “forget time”. But the question hides surprising conceptual depth and led to an active line of research in the 2000s, with landmark results by Melliès and Boudes among others.

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.

Session-typed programming languages help programmers correctly implement communicating systems. Though many techniques exist for reasoning about these languages and their processes, few treat general recursive types and few are compositional. As a consequence, they cannot be applied to many useful programs and they do not support modular reasoning. In this talk, I will present a denotational semantics for Polarized Intuitionistic Processes (PIP), a session-typed proofs-as-processes interpretation of polarized intuitionistic linear logic. PIP features general recursion, channel transmission, choices, and synchronization. This semantics generalizes Kahn’s semantics for dataflow networks to support bidirectional, session-typed communication. It supports modular reasoning and validates expected program equivalences. Moreover, it is sound relative to barbed congruence (the canonical behavioural notion of process equivalence), and it is fully abstract in the absence of negative channel transmission. As a result, our semantics provides an intuitively reasonable account of session-typed communication and a foundation for reasoning about processes in more realistic session-typed languages.

In this talk, I will introduce open parity games, which form a compositional approach to parity games. On the syntactic level, these open games are defined as string diagrams, and can be thought of as traditional parity games augmented with open ends. Our goal is to show that computing the set of winning positions in such a game can be done compositionally on the string diagram. To this end, we introduce a suitable semantics inspired by the work by Grellois and Melliès on the semantics of higher-order model checking. This semantics coincides with the notion of winning position when there are no open ends and can be computed compositionally on the syntax.

A key concept of higher topos theory involves the existence of universes, either by definition (in the elementary case) or by construction (in the Grothendieck case). In this talk we want to illustrate how comprehending the category theory of internal universes could help us internalize a variety of key constructions. This would allow us to obtain results known in the classical setting in an elementary higher topos. No prior knowledge of higher category theory of any form will be assumed.

Une introduction au problème du mot, lien entre sa complexité et la théorie géométrique des groupes, en particulier avec les cônes asymptotiques.

This talk is about the semantics of commutative combinations of effects.

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.

De Vries (1962) obtained a categorical duality for the category KHaus of compact Hausdorff spaces and continuous functions. The objects of the dual category DeV are complete boolean algebras equipped with a proximity relation, known as de Vries algebras, and the morphisms are functions satisfying certain conditions. One drawback of DeV is that composition of morphisms is not usual function composition.

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

Lean's mathematical library mathlib is a rapidly growing unified library of formalized mathematics, with over 1 million lines of code. The library contains most of an undergraduate math curriculum, and many graduate topics. It is used as a basis to formalize advanced results in mathematics.

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.

Much of my recent research has been in demonstrating the idea that working with Ehrhard's notion of finiteness space forces certain sums which would a priori be infinite to become finite, and hence well-defined, without resorting to limit structure or infinitary computations. It is hoped that this will lead to a great many applications, and that one of those applications is in the field of monoidal topology. Typically monoidal topology takes place in the category of quantale-valued relations.

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.

In my talk I will show that some versions of operads/multicategories (non-Sigma, symmetric, with amalgamations) and finitary polynomial and analytic functors, i.e., the devices that have been used to define opetopic sets by various authors, are either very closely related or even two sides of the same coin, if placed in the suitable context. These structures have been used in many contexts and not always with the understanding to what extent they are similar.

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.

Over the past ~5 years, a number of authors trying to apply methods from category theory to game theory, machine learning, and dynamical systems, have noticed a strong convergence. It seems that very similar categorical structures emerge from the study of all of these things, centering around the notion of /lens/. I'll give a survey of this research program and sketch some recent advances.

Two syntactic classes of theories play preponderant rôles in traditional category-theoretic universal algebra: algebraic (a.k.a. “Lawvere” or “Lawvere-Bénabou”) theories, and essentially algebraic theories (introduced by Freyd). Models of the former are precisely Set-based algebraic structures that can be defined using finite products, while those of the latter are Set-based algebraic structures that can be defined using finite limits. Theories in each of these classes are defined using simple (i.e. non-dependent) sorts, and the generalisation from Lawvere-Bénabou theories to essentially algebraic theories involves allowing certain partial functions in addition to total functions. 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.

Two syntactic classes of theories play preponderant rôles in traditional category-theoretic universal algebra: algebraic (a.k.a. “Lawvere” or “Lawvere-Bénabou”) theories, and essentially algebraic theories (introduced by Freyd). Models of the former are precisely Set-based algebraic structures that can be defined using finite products, while those of the latter are Set-based algebraic structures that can be defined using finite limits. Theories in each of these classes are defined using simple (i.e. non-dependent) sorts, and the generalisation from Lawvere-Bénabou theories to essentially algebraic theories involves allowing certain partial functions in addition to total functions.

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.

Counting associative structures has been presented for many years in different applications and techniques, for examples counting finite groups, semigroups and monoids, etc.. In our work, we extend the count to finite categories. Our aim is to analyze the structure of finite categories, and develop structure theorems for these. We use McCune's Prover9/Mace4 to construct models, providing in particular a count of the number of categories with two non-isomorphic objects and such that all hom-sets have size 3. As a result of our counting, we obtain that the algebraic structure of monoids in categories is very important in the classification problem. For example, we will present a classification of a specific kind of monoids called “grouplike”, these are monoids that contain a group plus an ordered set of identities. Studying grouplike categories clarifies greatly the enumeration question and the numbers that are obtained from the counting.

On appelle équivalence de Kan-Quillen l'équivalence de Quillen entre ensembles simpliciaux et espaces topologiques donnée par l'adjonction entre realisation géométrique et ensemble simplicial des simplexes singuliers. L'équivalence entre ces deux catégories modèles est un résultat fondateur de la théorie de l'homotopie. Une bonne notion de théorie de l'homotopie stratifiée devrait reproduire ce résultat. Dans cet exposé, je présenterai la construction de catégorie modèles d'espaces et d'ensembles simpliciaux stratifiés, et j'expliquerai pourquoi l'équivalence de Kan-Quillen, dans ce contexte, n'est obtenue que sous la forme d'une équivalence entre catégories infinies.

La pro-complétion, et sa duale la ind-complétion, jouent des rôles majeurs en informatique théorique, en théorie des catégories et en géométrie algébrique notamment. L'exemple type est la catégorie des espaces de Stone qui est la pro-complétion de la catégorie des ensembles finis. Dans la littérature, il a été montré que quelques propriétés se transfèrent d'une catégorie à sa pro-complétion. C'est le cas des propriétés d'être une catégorie régulière, co-régulière, additive, abélienne ou encore extensive. Dans cet exposé, nous formulerons un théorème qui englobe tous ces résultats et donne pléthore de nouveaux exemples. Appliqué à la catégorie des ensembles finis, nous en déduirons que la catégorie Stone est cohérente, extensive, distributive, régulière, co-régulière, co-arithmétique, co-Mal'tsev, co-protomodulaire etc. Afin d'énoncer le théorème principal, nous introduirons une notion de séquents d'exactitude, qui permet d'encoder une grande variété de propriétés catégoriques. Cet exposé est basé sur un travail en collaboration avec Zurab Janelidze

We introduce judgemental theories and their calculi to frame type theory and proof theory in the same mathematical framework. Our analysis sheds light on both the topics, providing a new point of view. In the case of type theory, we provide an abstract definition of type constructor featuring the usual formation, introduction, elimination and computation rules. In proof theory we offer a deep analysis of structural rules, demystifying some of their properties, and putting them into context. We finish the paper discussing the internal logic of a topos, a predicative topos, an elementary 2-topos et similia, and show how these can be organized in judgemental theories.

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

In this talk I will describe four approaches to the semantics of linear logic, focusing on the multiplicative fragment of classical linear logic. I will also explain how these are related.

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.

The differential calculus uses addition in a crucial way: this appears clearly in the Leibniz Rule. This is why the differential lambda-calculus as well as differential linear logic feature an unrestricted addition operation on terms (or proofs) of the same type. From an operational point of view, this means that these formalisms feature finite non-determinism. So a natural question arises: is non-determinism inherent to any differential extension of the lambda-calculus and linear logic? Based on intuitions coming from probabilistic coherence spaces, we provide a negative answer to this question, introducing a setting of “summable categories” where the notion of summable pairs of morphisms is axiomatized by means of a functor equipped with three natural transformations satisfying a few axioms. Then we define a notion of differentiation in such a summable category equipped with a resource modality (exponential in the sense of linear logic): this differential structure is a distributive law between a monad associated with the summability structure and the resource comonad, satisfying a few additional axioms. I will present various aspects of this theory (which features similarities with tangent categories), concrete instances of the theory as well as the syntax of a differential version of PCF which can be derived from this general categorical setting. In particular I will show that coherence spaces provide a model of this coherent differentiation, in sharp contrast with differential linear logic.

The differential calculus uses addition in a crucial way: this appears clearly in the Leibniz Rule. This is why the differential lambda-calculus as well as differential linear logic feature an unrestricted addition operation on terms (or proofs) of the same type. From an operational point of view, this means that these formalisms feature finite non-determinism. So a natural question arises: is non-determinism inherent to any differential extension of the lambda-calculus and linear logic? Based on intuitions coming from probabilistic coherence spaces, we provide a negative answer to this question, introducing a setting of “summable categories” where the notion of summable pairs of morphisms is axiomatized by means of a functor equipped with three natural transformations satisfying a few axioms. Then we define a notion of differentiation in such a summable category equipped with a resource modality (exponential in the sense of linear logic): this differential structure is a distributive law between a monad associated with the summability structure and the resource comonad, satisfying a few additional axioms. I will present various aspects of this theory (which features similarities with tangent categories), concrete instances of the theory as well as the syntax of a differential version of PCF which can be derived from this general categorical setting. In particular I will show that coherence spaces provide a model of this coherent differentiation, in sharp contrast with differential linear logic.

The differential calculus uses addition in a crucial way: this appears clearly in the Leibniz Rule. This is why the differential lambda-calculus as well as differential linear logic feature an unrestricted addition operation on terms (or proofs) of the same type. From an operational point of view, this means that these formalisms feature finite non-determinism. So a natural question arises: is non-determinism inherent to any differential extension of the lambda-calculus and linear logic? Based on intuitions coming from probabilistic coherence spaces, we provide a negative answer to this question, introducing a setting of “summable categories” where the notion of summable pairs of morphisms is axiomatized by means of a functor equipped with three natural transformations satisfying a few axioms. Then we define a notion of differentiation in such a summable category equipped with a resource modality (exponential in the sense of linear logic): this differential structure is a distributive law between a monad associated with the summability structure and the resource comonad, satisfying a few additional axioms. I will present various aspects of this theory (which features similarities with tangent categories), concrete instances of the theory as well as the syntax of a differential version of PCF which can be derived from this general categorical setting. In particular I will show that coherence spaces provide a model of this coherent differentiation, in sharp contrast with differential linear logic.

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way. While very promising, this methodology was previously not fully formalised and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalising the lower-level details, which together enable constructing fully machine-checked crypto proofs in the Coq proof assistant. Moreover, SSProve is itself formalised in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky. Howe (1989) gave a direct proof that it is a congruence. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name and call-by-value λ-calculus, as well as in a simple non-deterministic variant.

This is joint work with Ambroise Lafont.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky. Howe (1989) gave a direct proof that it is a congruence. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name and call-by-value λ-calculus, as well as in a simple non-deterministic variant.

This is joint work with Ambroise Lafont.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky. Howe (1989) gave a direct proof that it is a congruence. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name and call-by-value λ-calculus, as well as in a simple non-deterministic variant.

This is joint work with Ambroise Lafont.

We show that for any quantale Q, a Q-category is skeletal and complete if and only if it is injective with respect to fully faithful Q-functors. This is a special case of known theorems due to Hofmann and Stubbe, but we provide a different proof, using the characterisation of the MacNeille completion of a Q-category as its injective envelope.

Differential categories provides the categorical semantics of differential linear logic. In particular, differential categories come equipped with an exponential modality, which categorically speaking is a comonad, and where the differential structure is captured by a natural transformation called the codereliction. CoKleisli categories of differential categories are well studied, they are Cartesian differential categories, or in other words, categorical models of the differential lambda calculus. On the other hand, coEilenberg-Moore categories of differential categories (.i.e the category of coalgebras of the comonad) are less-well studied.

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

In 'A practical type theory for symmetric monoidal categories’ M. Shulman presents a type theory in which we may reason about symmetric monoidal categories as if they were categories of 'sets with elements' with one major caveat: whereas in Set elements of products are 'decomposable', terms of product types in PTT are 'not necessarily decomposable’.

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

The goal of this work is to get a better understanding of the type Sn=Sn where Sn is the sphere of dimension n, inductively defined by repeated suspensions. I will first prove in full details that S1=S1 is equivalent to S1+S1 (the disjoint sum of two copies of the circle), and explain why it is highly unrealistic to conjecture a straightforward generalization for Sn. However, part of the argument for S1 can be extended in higher dimensions to prove that Sn=Sn has two equivalent connected components, one centered at the identity function and one centered at its “opposite” (to be defined properly during the talk). This generalization is done by induction on n, and the case n=1 does not constitutes a good base case. Consequently I will detail the case n=2 (interesting in its own), and sketch the induction step for n>3. This is joint work with M.Bezem and N.Kraus.

We discuss a simple Turing-complete extension of first-order logic FO. The extension adds two new features to FO. The first one of these is the capacity to add new points to models and new tuples to relations; the corresponding deletion operators are also introduced. The second new feature is a construct that allows formulae to refer to themselves. We survey some of the principal properties of this logic and its extensions with, e.g., generalized quantifiers.

The General Adjoint Functor Theorem of Freyd has a straightforward extension to the enriched setting. There is also a Weak Adjoint Functor Theorem, due to Kainen, and providing a sufficient condition for the existence of a weak left adjoint, where weakness refers to the existence but not uniqueness of factorizations. I will report on recent joint work with Steve Lack and Lukas Vokrinek, in which we prove a weak adjoint functor theorem in the enriched context. This actually contains the other three theorems as special cases. Our base for enrichment will be a monoidal model category. Our motivating example involves simplicially enriched categories, where the base category of simplicial sets is equipped with the Joyal model structure. The theorem then has applications to the Riehl-Verity theory of infinity-cosmoi.

Cet exposé sera une introduction à l'algèbre linéaire graphique (graphical linear algebra), un langage qui permet de raisonner de façon compositionnelle à propos de système R-linéaires, pour divers semi-anneaux R. Lorsque que R est un corps, sa sémantique et sa théorie équationnelle sont bien comprises. Dans ce contexte, l'algèbre linéaire graphique est proche des signal flow graphs, un autre langage communément utilisé en théorie du contrôle pour spécifier des systèmes dynamiques au comportement linéaire. Des travaux récents ont montrés que, pour R = ℕ, la même syntaxe graphique permet de spécifier des systèmes concurrents qui manipulent des ressources discrètes. On obtient alors un langage suffisamment expressif pour y encoder très naturellement tous les réseaux de Petri et raisonner de façon modulaire à propos de leur comportement. Nous donnerons des axiomatisations complètes pour ces différentes interprétations et étudierons leurs extensions affines.

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

The DeepSpec research project is a cross institution, cross project investigation to push further the science of specification and verification of software artifacts. Its ambition is crystallized into four qualities that specifications should have: they should be rich, live, two-sided and formal.

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.

Accessible categories with directed colimits have proven to be a suitable framework to develop abstract model theory and generalize the notion of abstract elementary class, quite relevant in model theory. For every accessible category with directed colimits A, one can define its Scott topos S(A). This construction is the categorification of the Scott topology over a poset with directed unions, and thus provides a geometric understanding of accessible categories. S(A) represents also a candidate axiomatization of A, in the sense that the category of points of the Scott topos (i.e., the models of the theory that it classifies) is very often a relevant hull of A. During the talk we introduce the Scott construction and explain both its geometric and logical aspects.

We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains. The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators. We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.

Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this talk we discuss how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics. Joint work with Romain Péchoux, Simon Perdrix and Mathys Rennela.

Finite-precision floating point arithmetic introduces rounding errors which are traditionally bounded using a worst-case analysis. However, worst-case analysis might be overly conservative because worst-case errors can be extremely rare events in practice. Here we develop a probabilistic model of rounding errors with which it becomes possible to quantify the likelihood that the rounding error of an algorithm lies within a given interval.

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.

The μ-calculus with atoms, or nominal μ-calculus, is a temporal logic for reasoning about transition systems that operate on data atoms coming from an infinite domain and comparable only for equality. It is, however, not expressive enough to define some properties that are of interest from the perspective of system verification. To rectify this, we extend the calculus with tests for atom freshness with respect to the global history of transitions. Since global histories can grow arbitrarily large, it is not clear whether model checking for the extended calculus is decidable. We prove that it is, by showing that one can restrict attention only to locally relevant parts of the history.

Recursion is a great tool to create readable programs and for proof discovery. Unrestricted recursion, however, leads to non-termination and thereby makes reasoning about programs harder and may make a logic inconsistent. Guarded recursion, on the other hand, allows us to control recursion in programs and proofs. The basic idea is to extend types or formulas with a modality, usually called the later modality, and a few rules that allow the controlled introduction of recursion. This control ensures termination of programs and consistency of proofs.

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

There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebras, another one is open maps. In this talk, I will describe these two approaches, illustrated by the case of labelled transition systems (almost no knowledge in category theory is needed for this part). I will then describe how it is possible to translate one into the other in some cases. From open maps to coalgebras, this was done by Lasota, using multi-sorted transition systems. From coalgebras to open maps, this was done in my joint work with Thorsten Wißmann, Shin-ya Katsumata and Ichiro Hasuo, where we derived path-categories and trace semantics for free for different flavors of categories of coalgebras with non-deterministic branching. I will illustrate those constructions on various concrete examples (tree automata, regular nominal automata, …).

We introduce a new type of algebra, the Expedient Algebra EXP, for which computations satisfy tight distribution control. Algorithms satisfying such distribution control are guaranteed to support modular time analysis–drastically simplifying static timing. The property ensures that problematic algorithms, for which the exact time is too hard or impossible to analyze with current means can be distinguished at code level from algorithms supporting an elegant modular time analysis. Little is known about the intrinsic properties of algorithms exhibiting such distribution control.

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.

La traduction naïve des structures ensemblistes dans la théorie des types de Martin-Lof est souvent incomplète: sans hypothèses auxiliaires, comme la decidabilité de l'égalité ou troncation, ces traductions ne spécifient pas le comportement de la structure par rapport aux égalités supérieures. Par contre, une description complète n'est pas facile puisque celle-ci exige un nombre infini d'équations. Je présenterai des progrès récent sur ce problème en donnant une définition d'une “monade polynomiale” interne à la théorie des types.

The talk gives an overview of our several works on programming language 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.

A cornerstone of the theory of λ-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho’s system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.

We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs à la Scott through the use ordered Banach spaces which allow definitions in terms of fixed points. Being based on a monoidal rather than cartesian closed structure, our semantics effectively treats randomness as a resource.

Je rappelle, pour fixer les notations, que si S est une catégorie, et F: S° —> CAT est un lax foncteur, cette construction fournit une catégorie Gr(F) munie d’une préfibration Pr(F): Gr(F)—>S qui est une fibration ssi F est un pseudo-foncteur. Questions: Par quel type de bi, ou 2, catégorie K peut on remplacer CAT ? Quelles propriété a la correspondance F —> Gr(F) Peut-on internaliser cette construction i.e. si E est, par exemple, un topos, peut-on remplacer S par une catégorie interne à E et CAT par la 2-catégorie CAT(E) des catégories internes à E. La liste ci-dessus est loin d’être exhaustive. Je tâcherai, sans lasser l’auditoire, de montrer la grande variété des questions…, et des réponses.

Many complex generative systems use languages to create structured objects. We consider a model of random languages, defined by weighted context-free grammars. As the distribution of grammar weights broadens, a transition is found from a random phase, in which sentences are indistinguishable from noise, to an organized phase in which nontrivial information is carried. This marks the emergence of deep structure in the language, and can be understood by a competition between energy and entropy.

We provide syntactic (expression-level) language derivative operations, both in the styles of Brzozowski and Antimirov, for trace closures of regular word languages wrt. an independence relation on the alphabet. The Brzozowski and Antimirov style derivatives essentially define functional resp. relational small-step operational semantics of an (abstracted) sequential programming language where some instructions, given by the independence relation, can be reordered without any observable consequences. Our development is motivated by the fact that some aspects of relaxed memories can be explained by allowing the threads of a concurrent program to be reordered in this manner.

We consider Ribenboim’s construction of rings of generalized power series. Ribenboim’s construction makes use of a special class of partially ordered monoids and a special class of their subsets. While the restrictions he imposes might seem conceptually unclear, we demonstrate that they are precisely the appropriate conditions to represent such monoids as internal monoids in an appropriate category of Ehrhard’s finiteness spaces. Ehrhard introduced finiteness spaces as the objects of a categorical model of classical linear logic, where a set is equipped with a class of subsets to be thought of as finitary. Morphisms are relations preserving the finitary structure.

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.

On utilise les régularités des morphismes de la catégorie cartésienne fermée des espaces cohérents probabilistes pour majorer une distance naturelle sur les (classes d'équivalence observationnelle) de termes de PCF probabilistes par une distance définissable dans le modèle.

Game semantics is the art of interpreting formulas (types) as games and proofs (programs) as strategies interacting in space and time with their environment. In order to reflect the interactive behaviour of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a purely sequential programming language, the program (Player) and its environment (Opponent) play one after the other, in a strictly alternating way. In the case of a concurrent language, on the other hand, Player and Opponent are allowed to play several moves in a row, in a non alternating way. In the two cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronise properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this talk, I will introduce the notion of template game and exhibit a number of simple and fundamental combinatorial properties which ensure that a given scheduling policy defines a monoidal closed bicategory of games, strategies and simulations. The notion of template game will be illustrated by constructing two game models of linear logic with different flavors (alternating and non alternating) using the same categorical combinatorics, performed in the category of small categories.

Differential categories were introduce to provide a minimal categorical semantics for differential linear logic. However, there exists three approaches to axiomatizing the derivative by deriving transformations, coderelictions, and creation maps - long thought to be distinct notions. Recently, Blute, Cockett, Seely and myself have revisited the axioms of a differential category and showed that for categorical models of differential linear logic the three approaches are equivalent. Thus, there is only one notion of differentiation.

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.

Rauszer's bi-intuitionistic propositional logic (BiInt) is the conservative extension of intuitionistic propositional logic (Int) with a connective dual to implication usually called 'exclusion'. A *standard-style* sequent calculus for BiInt is easily obtained by extending the multiple-conclusion sequent calculus of Int with exclusion rules dual to the implication rules. However, similarly to standard-style sequent calculi for modal logics like S5, this calculus is incomplete without the cut rule. Cut-freeness is achievable for sequent calculi with non-standard sequent forms. The *nested* and *labelled* calculi (Goré, Postniece; Pinto, Uustalu) were motivated by quite different intuitive considerations. Yet they turn out to be very close on the technical level: slightly adjusted towards each other, they can be made isomorphic.

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

I will introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the speaker's previous method called categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces. I will also talk about the liftings of algebraic operations to the codensity-lifted monads. If time permits, I will mention a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.

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

Intersection Types are a well-known family of tools that characterise different notions of normalisation. We develop a general framework for building such systems from a notion of approximation, that allows to recover many well-known intersection type systems, as well as new systems, for every calculus that can be translated into linear logic. This construction uses in a crucial way Melliès and Zeilberger’s “type systems as functors” viewpoint, as well as an adapted Grothendieck construction.

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

Universal algebra uniformly captures various algebraic structures, by expressing them as equational theories or (abstract) clones. The ubiquity of algebraic structures in mathematics has also given rise to several variants of universal algebra, such as symmetric and non-symmetric operads, clubs, and monads. In this talk, I will present a unified framework for these cousins of universal algebra, or 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.

F* is a programming language providing proof-assistant features such as dependent types, a rich logic with universes and tactics. Its primary goal is to implement security critical program e.g. cryptographic primitives (HACL*) or protocols (HTTPS in MiTLS), prove gradually their correction and extract to performant effectful low-level code. In order to achieve gradual proof of effectful code, F* relies on weakest-precondition indexed monads called Dijkstra monads. In this presentation we will explain why and how Dijkstra monads are used in F*, as well as how they are often derived from usual presentations of monads as can be found in more mainstream language such as Haskell.

n-fold categories are obtained by n-iterations of the internal category construction, starting from the category Cat. N-Fold categories satisfying the globularity condition correspond to strict n-categories. One can ask if there is an intermediate structure between n-fold categories and strict n-categories which is a model of weak n-categories. We answer this question positively with the introduction of the category of weakly globular n-fold categories. This category is based on a new paradigm to weaken higher categorical structures, and offers several advantages in terms of applications. We will illustrate how this model is part of a wider class of Segal-type models, and its equivalence with the Tamsamani-Simpson model of weak n-categories.

To describe systems composed of interacting parts, scientists and engineers draw diagrams of networks: flow charts, Petri nets, electrical circuit diagrams, signal-flow graphs, chemical reaction networks, Feynman diagrams and the like. In principle all these different diagrams fit into a common framework: the mathematics of symmetric monoidal categories. This has been known for some time. However, the details are more challenging, and ultimately more rewarding, than this basic insight. Two complementary approaches are presentations of symmetric monoidal categories using generators and relations (which are more algebraic in flavor) and decorated cospan categories (which are more geometrical). In this talk we focus on the latter.

The talk presents the theorems of Myhill-Nerode and Chomsky-Schützenberger using rewriting diagrams of semi-Thue systems as paradigm example of planar acyclic circuit diagrams (PLACIDs)—the “graphical syntax” of monoidal categories. The talk will focus on the proposal of a definition of recognizable language in a monoidal category, namely sets of arrows that coincide with the inverse image of their direct image under a monoidal functor to a finite monoidal category. For the case of PLACIDs, this class of languages is shown to coincide with the languages of automata in the sense of Bossut, under modest assumptions on gates of circuit diagrams; moreover, the usual notion of recognizable tree language is recovered. The talk presents the Myhill-Nerode theorem as a tool for solving Bossut's open problem of automata complementation. The remainder of the talk describes work in progress and future work, in particular the Chomsky-Schützenberger theorem for PLACIDs.

Contrary to traditional formulations of rewriting, which tend to rely on ideas such as category-theoretic double pushout constructions, the novel rule algebra framework is based upon the idea of interpreting rewriting rules as generators of certain diagrammatic algebras. In this whiteboard talk, I will present the core mathematical ideas and results, including the deep link between certain types of combinatorial Hopf algebras and rewriting theories. Some illustrative examples for the cases of discrete and graph rewriting will be provided.

Following the pattern of the Frobenius structure usually assigned to the 1-dimensional sphere, we investigate the Frobenius structures of spheres in all other dimensions. Starting from dimension $d=1$, all the spheres are commutative Frobenius objects in categories whose arrows are ${(d+1)}$-dimensional cobordisms. With respect to the language of Frobenius objects, there is no distinction between these spheres—they are all free of additional equations formulated in this language. The corresponding structure makes out of the 0-dimensional sphere not a commutative but a symmetric Frobenius object.

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

It turns out that enumeration of graphs embedded on surfaces (an active area of combinatorics since Bill Tutte's pioneering work in the 1960s) has a variety of surprising links to the combinatorics of lambda calculus. In the talk, I will give a brief survey of these enumerative connections, then focus on the 1-to-1 correspondence (originally described in work by Bodini, Gardy, and Jacquot) between linear lambda terms and rooted trivalent maps. The key to understanding this bijection will be combining an interpretation of lambda terms as string diagrams with a Tutte-style decomposition of rooted trivalent maps with boundary. Finally, if time permits, I will discuss a suggestive analogy between typing and edge-coloring, and use this to motivate a deeper study of the surprisingly subtle typing properties of linear lambda terms.

We investigate monads of partiality in Martin-Löf type theory, following Moggi’s general monad-based method for modelling effectful computations. These monads are often called lifting monads and appear in category theory with different but related definitions. In this talk, we unveil the relation between containers and lifting monads. We show that the lifting monads usually employed in type theory can be specified in terms of containers. Moreover, we give a precise characterization of containers whose interpretations carry a lifting monad structure. We show that these conditions are tightly connected with Rosolini’s notion of dominance. We provide several examples, putting particular emphasis on Capretta’s delay monad and its quotiented variant, the non-termination monad.

It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this talk we will present such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from \LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the idea that LL is, in fact, a ``universal framework'' for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of LL featuring different axioms for its modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for different logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems.

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

There is a growing interest in programs proofs checked by computer. Proofs about programs are often very long and have to face a huge amount of cases due to the multiplicity of programs variables and the precise details of the programs. This is very frustrating since we would like to explain the proofs of correctness and publish them in scientific articles. However if one considers simple algorithms, we would expect to explain their proofs of correctness in the same way as we explain a mathematical proof for a non too complex theorem.

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.

Type systems based on linear logic and their friends have proved that they are both capable of expressing a wealth of interesting abstractions. Among these the ability to mix garbage-collected and explicitly managed data in the same language. This is of prime interest for distributed computations that need to reduce latency induced by GC pauses: a smaller GC heap is a happier GC heap.

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.

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

The lambda-calculus studies the dynamics of computation, but the complexity of one computation path cannot be forecast, neither in time nor in space, and there is no direct control on the execution environment.

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.

Les tableaux de Young portent une multiplication associative, décrite par l'algorithme de Schensted. Le monoïde ainsi obtenu est appelé plaxique. Il joue un rôle fondamental dans de nombreuses applications combinatoires et algébriques. On montrera que cette multiplication sur les tableaux est entièrement déterminée par un tressage sur l'ensemble (bien plus simple !) des colonnes. Ici un tressage est une solution ensembliste de l'équation de Yang-Baxter. Notre tressage s'inscrit également dans le cadre de la réécriture. Comme application, on identifiera la cohomologie de Hochschild du monoïde plaxique, qui résiste à toutes les approches classiques, à la cohomologie tressée des tableaux-colonnes, beaucoup plus accessible. Toutes les notions et constructions seront rappelées.

Plusieurs modèles de sémantique de jeux concurrents ont émergé ces dernières années. Dans ce travail, on se concentre sur certaines de ces approches, qui ont donné des modèles de CCS, du pi-calcul et du lambda-calcul non-déterministe. Un point commun informel mais saillant entre ces approches est que les stratégies innocentes sont définies commes les faisceaux pour la topologie de Grothendieck où les parties sont recouvertes par leurs vues. On propose ici de tisser un lien formel entre deux de ces approches au niveau des parties et des stratégies.

Program differences are pervasive in software development, but most of the time they are represented as textual differences with no regards to the syntactic nature of programming languages or their semantics. Thus, they may be hard to read and often fail to convey insight on the changes on semantics. Furthermore, such low-level, unstructured presentations are hard to reason about.

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)

Call-by name (CBN) and call-by-value (CBV) have been defined as the dual solutions to a critical pair at the heart of cut-elimination in classical sequent calculus. When one moves to intuitionistic logic, this symmetric picture breaks, but what happens precisely? How are such definitions adapted to the intuitionistic case? How do the resulting calculi relate to the many other proposals for intuitionistic CBV and CBN calculi? And what does that break of duality say about intuitionistic logic? We find that proof-theory alone distills new CBV and CBN lambda-calculi which agree, in a technical sense, with the computational lambda-calculus and the ordinary lambda-calculus, respectively; but the former distilled calculus is contained in the latter - a vindication of Plotkin. This containment, in turn, rests on another asymmetry: a certain permutative/focalization conversion, named T, solves what remains of the classical critical pair in favor of CBN, while the symmetric solution with a certain CBV conversion Q does not exist. In this sense we may say intuitionistic logic enjoys a CBN bias. Full answers to the above questions require us to work simultaneously with sequent calculus and its equivalent bidirectional natural deduction. The former syntax is our starting point, where we track the (lost) symmetries and find the idea of permutative conversions; the latter syntax is the bridge towards more traditional programming notations. For instance, only in bidirectional natural deduction one sees that T eliminates the difference between “let” and explicit substitution, and only there one understands what calling paradigm corresponds to the superimposition of CBN and CBV.

I will present AEON (Atomic Events and Ownership Networks), a programming model for safe and scalable cloud computing. AEON is based on the well-known paradigms of object-orientation and event-driven programming. AEON’s runtime system guarantees a linearizable and deadlock-free semantics for events that span across multiple objects and servers. Moreover, to achieve an economical and scalable solution, our runtime system provides seamless elasticity (the capability to adapt the resources usage to the actual workload), and exploits the object graph — the ownership network — to enhance parallelism. In this talk will concentrate on the safety aspects of the semantics of AEON, and show some experimental scalability results.

We prove a finite family developments theorem (FFD) for the calculus with explicit substitutions Linear Substitution Calculus (LSC). The notion of redex family is obtained by adapting Lévy labels to support the two distinctive features of LSC, namely its use of context rules that allow substitutions to act “at a distance” and also the set of equations modulo which it rewrites. We then apply FFD to prove a number of results for LSC including: an optimal reduction result, an algorithm for standardisation by selection, and normalisation of a linear call-by-need reduction strategy.

For years we have been bothered by a small mistery on categorical models of Linear Logic (star-autonomous categories) and Geometry of Interaction (compact closed categories, typically arising from traced monoidal categories via Int-construction): is there a proper intermediate structure between star-autonomous categories and compact closed categories, that is, a traced star-autonomous category which is not compact closed? We settle this issue by showing that any traced star-autonomous category is actually 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.

I will begin by presenting a structural description of the kind of empirical data which arises in physical experiments, using the language of sheaf-theory. A potential feature of such data is contextuality (including as a special case non-locality) which can be neatly characterised in this setting. The feature does not arise in classical data, and a number of recent results indicate that it is the key feature in enabling quantum advantages or speedups over classical behaviour in a variety of computational scenarios. The sheaf-theoretic perspective exposes a qualitative hierarchy of strengths of contextuality and I will also mention recent efforts to quantify contextuality via linear programming. Finally I will report on work in progress on developing a resource theory for contextuality, beginning with an algebra of empirical models under whose operations contextuality is monotonically decreasing.

In the usual deterministic lambda-calculus the confluence of the unique computation rule, the beta-reduction, makes it easy to turn the reduction into an equality, the beta-equivalence. This idea to consider not computation but equalities on terms gives rise to the notion of lambda-theory. On the other hand the probabilistic lambda-calculus is usually treated only in terms of computation. In particular we know that we must impose a reduction strategy for the probabilistic choice if we want the calculus to make sense.

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.

The Krivine machine is an abstract machine implementing the linear head reduction of $\lambda$-calculus. Ehrhard and Regnier gave a resource sensitive version returning the annotated form of a $\lambda$-term accounting for the resources used by the linear head reduction. These annotations take the form of terms in the resource $\lambda$-calculus.

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$.

Propositional dynamic logic (PDL) is at the core of reasoning about dynamic systems. We present a syntax directed formalism for PDL, built on coproofs.

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.

Il existe deux formalisations des langages/systèmes probabilistes: l'une est de considérer l'arbre des dérivations (avec branchements probabilistes), l'autre est de considérer des distributions de probabilités. Avoir accès à l'arbre de dérivation est pratique pour les preuves car on a accès à l'historique complet, mais lorsque l'arbre est infini, le formalisme est très lourd et peu explicite. La formulation à base de distributions est plus simple et donne des théorèmes élégants mais engendre des preuves très complexes (où il faut souvent retrouver l'historique du calcul). Dans cet exposé nous verrons qu'il est possible de récupérer le meilleur des deux mondes grâce à un théorème d'encodage probabilistique inspiré de la théorie catégorique des coalgèbres. Nous verrons qu'il s'agit d'un outil systématique qui, à l'instar de l'induction ou la coinduction, permet de structurer des preuves et des définitions complexes. Pour des raisons de temps, nous n'évoquerons que brièvement comment ce schéma de preuve nous permet de redéfinir une version probabiliste de notions usuelles telles que les types intersection probabilistes ou les candidats de réductibilité probabilistes.

Most standard models of the lambda calculus validate the principles of infinitary rewriting (which include identification of meaningless terms). For example, in Scott models, the interpretation of every fixed point combinator is equal to the limit (in the model) of interpretations of

\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.