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.