9:00-10:00
Pawel Sobocinski: Adhesive categories, Van Kampen squares and bicolimits. [slides]
In 2004 Steve Lack and myself introduced adhesive categories, which have since been widely used as a mathematical foundation for graph rewriting (for instance, via the double pushout approach). Adhesive categories follow in the tradition of extensive categories in that particular colimits (coproducts in extensive categories, certain pushouts in adhesive categories) "behave well" with respect to pullbacks. The colimits in question can be characterised in an elementary fashion: they satisfy what has become known as the Van Kampen condition. In recent work with Tobias Heindel we have characterised this condition as a universal property---a colimit satisfies the Van Kampen condition exactly when it is a bicolimit when embedded into the canonical bicategory of spans.
10:00-10:30
Jean-Guillaume Dumas: Sequential computation and cartesian effect categories. [slides]
Most often, in a categorical semantics for a programming language, the substitution of terms is expressed by composition and finite products. However this does not deal with the order of evaluation of arguments, which may have major consequences when there are side-effects. We first present a characterisation of effects and then provide a generalization of the binary product, called the sequential product. The universal property of this sequential product provides the obtained Cartesian effect categories with a powerful tool for constructions and proofs. We illustrate the notions on several examples of effects in programming languages: exception, partiality or state, and compare our approach with strong monads, Freyd-categories and Haskell's Arrows.
10:30-11:00
PAUSE
11:00-11:30
Tom Hirschowitz: Algebraic structures from shapes. [slides]
An important part of categorical computer science, at least in proportion, consists of extracting the algebraic essence of computational structures. The mother of all examples of this is the correspondence between simply-typed lambda-calculus and cartesian closed categories. Presenting such algebraic structures can be subtle, especially when seeking so-called coherence, which exhibits the equivalence of algebra with some combinatorial structure. The talk is an introduction by example to a technique for constructing algebraic structures from their expected combinatorial description, bypassing the tedious work of presentation. The pattern is as follows: (1) the combinatorial description provides a monad which yields the expected structure (2) the Leinster-Weber theory of local right adjoint monads generates a presentation for it. 
11:30-12:00
Philippe Malbos: Homotopical methods in polygraphic rewriting. [slides]
We survey some homotopical properties of convergent presentations of n-categories. Using the notion of polygraph, we introduce the homotopical property of finite derivation type for n-categories, generalising the one introduced by Squier for word rewriting systems. We characterise this property by using the notion of critical branching. We generalise the notion of identities among relations, well known for presentations of groups, to presentation of n-categories by polygraphs. We relate identities among relation and critical branching.
12:00-12:30
Simon Perdrix: Categorical Quantum Computing: the necessity of Euler decomposition. [slides]
Categorical axiomatisation of quantum information processing has been initiated by Abramsky and Coecke. Coecke and Duncan recently introduced a categorical formalisation of the  interaction of complementary quantum observables. In this framework, we consider a new equation: the Euler decomposition of H, and demonstrate that a fundamental property of quantum entanglement is equivalent to this new axiom. Joint work with Ross Duncan (U. Oxford)
12:30-14:00
DEJEUNER
14:00-15:00
Pawel Sobocinski: The wire calculus. [slides]
The wire calculus is a process algebra for modelling truly concurrent systems with explicit network topologies. Instead of a Dijsktra-Hoare-Milner commutative parallel operator it features a non-communicating non-commutative parallel and an operator for synchronisation on a common boundary. The dynamics are handled by operators inspired by Milner's CCS and Hoare's CSP: unary prefix operation, binary choice and a standard recursion construct. The operational semantics is a labelled transition systems derived using SOS rules. The category with arrows the processes (terms modulo bisimilarity) is compact closed.
15:00-15:30
Olivier Laurent: Modèles catégoriques du lambda-calcul via la logique linéaire. [slides]
L'étude de la logique linéaire a fourni plusieurs traductions du lambda-calcul basées sur différentes décompositions linéaires de l'implication intuitionniste. Nous montrerons comment l'analyse catégorique permet d'interpréter ses traductions comme des constructions de modèles du lambda-calcul à partir de modèles de la logique linéaire.
15:30-16:00
PAUSE
16:00-16:30
Aurélien Pardon: Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs.
16:30-17:00
Frédéric Prost: Graph rewriting with polarized cloning. [slides]
In this talk we will investigate a novel approach to graph transformations with a particular focus on node cloning. We propose a graph rewriting framework where nodes can be cloned zero, one or more times. A node can be cloned together with all its incident edges, with only the outgoing edges, with only the incoming edges or without any of the incident edges. We show how pushout and pullback can be used in order to handle subtle graph transformations.  This framework subsumes previous works such as the sesqui-pushout, the heterogeneous pushout and the adaptive star grammars approaches.
17:00-17:30
Florian Hatat: Un lambda-calcul pour les catégories de réponse libres. [slides]
17:30-18:00
Dominique Duval: Deduction and Fractions. [slides]
A deduction rule H/C is a fraction C/H, so that the deduction process is the composition of fractions.



Pawel Sobocinski
Vincent Aravantinos
Alejandro Diaz-Caro