### Attendees and Abstracts

(Photographs by Brett Giles here)

(1) Ernie Manes (UMass, USA)

"Algebraic Models of Topological Dynamics: Coproduct Preserving Monads and Semigroups"

(slides here)
 Part I. The proximal relation. Part II. The role of semigroup theory. Part III. Generalizing compact metric spaces. Part IV. Finding examples

(2) Phil Mulry (Colgate, USA)

"Linear Functors and Modal Logic"

(slides here)

"Atlas groupoids and categories of fractions"

"Coproduct in inverse categories"

"Differential Turing categories"

"Combining Differential Categories with Manifolds"

We'll investigate what happens when one combines the cartesian differential categories of Blute, Cockett, and Seely with the manifold completion of Grandis. Our goal is to show that the resulting "smooth manifolds" always have tangent bundles, with the cartesian differential structure giving these tangent bundles many of their familiar properties.

"On the Total Maps of a Turing Category"

(15) Poalo Tranquilli (Lyon, France)

"Rewriting Aspects of Differential Linear Logic"

(slides here)

Much like proof nets, differential nets can be seen as a kind of string diagrams (or circuits) for differential linear categories. However while representations of categorical morphism are centered on commuting diagrams, i.e. equalities between composition of morphisms, nets are oriented towards rewriting theory. The issue is theorefore to orient equalities and to prove that such orientations enjoy good properties. In this talk we will present two rewriting systems for differential linear logic. On one side DiLL, corresponding to Ehrhard and Regnier's original differential nets (enriched with exponential boxes) and Fiore's creation maps. On the other DiLL$_{\partial\rho}$, closer to Blute, Cockett and Seely's differential categories and Fiore's creation and annihilation operators. We will present what issues arise when considering properties such as confluence or termination, and how both systems are to be considered "good" rewriting systems.

(16) Susan Niefield (Union College, USA)

"Exponentiability in Cat and Top via Double Categories"

(slides here)

For a small category B and a double category D, let LaxN(B,D) denote the category whose objects are vertical normal lax functors BD and morphisms are horizontal lax transformations.
It is well-known that LaxN(B,Cat) ≅Cat/B, where Cat is the double category of small categories, functors, and profunctors. In "Powerful Functors" (unpublished note), Street showed that a functor is exponentiable in Cat/B if and only if the corresponding normal lax functor is a pseudo-functor.
In the case where B is a finite poset, we subsequently generalized this equivalence to certain double categories. Examples include Cat as well as a double category Top whose objects are topological spaces. Our goal was to obtain an analogous characterization of exponentiable objects in Top/B. It turns out that, when B is a finite T0-space, a continuous map p: Y → B is exponentiable in Top/B if and only if the corresponding normal lax functor is a pseudo-functor and the pullback of p along every continuous map 2B is exponentiable in Top. Since every functor 2B is exponentiable in Cat, we have thus obtained the same condition for exponentiability in both Cat and Top.

(17) Ximo Diaz Boils (Valencia, Spain)

"Categorical characterizations of Burroni's recursion scheme"

Burroni's NNO and PL categories will be introduce in the context of similar structures over monoidal categories. Several characterizations will be presented in terms of different categorical concepts (Kan extensions, adjoints, coproducts,...). These were mentioned without any proof in the original paper: in this talk we will describe their proofs.

(18) Willem Bernard Heijltjes (Edinburgh, UK)

"Proof nets for sum--product logic"

(slides: part I and part II)

In linear logic, the prevailing semantics of the additive connectives and units is given by the categorical product and coproduct.  The logic of linear implication between strictly additive formulae, known as sum--product logic or additive linear logic, describes categories with free finite products and coproducts, up to an equational theory of proof permutations.  Deciding this theory is complicated by the presence of the units (the categorical initial and final objects) and the fact that in a free setting products and coproducts do not distribute.
In this talk I will present a novel solution to this decsion problem, in the form of a canonical, graphical representation of the categorical morphisms.  Starting with the existing proof nets for additive linear logic without uits, canonical forms are obtained by a remarkably simple graph rewriting algorithm.  I will sketch the outlines of the substantial correctness proof of this algorithm, and provide examples to highlight the difficulties of the decision problem.

"A differential model theory for resource lambda-calculi"

(slides: part I and part II)

In this talk we present a differential model theory for resource sensitive lambda-calculi based on differential categories. Such categories were introduced by Blute, Cockett and Seely to axiomatize categorically Ehrhard and Regnier's syntactic differential operator. We present an abstract construction for turning a symmetric monoidal category into a differential categories and we apply it to categories of games. In one instance, we recover a category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model, and shows how the differential combinator may be encoded in this language. A second instance corresponds to a new Cartesian differential category of games. We give a model of a Resource PCF in this category and show that it enjoys the finite definability property. Comparison with a semantics based on Bucciarelli, Ehrhard and Manzonetto's relational model reveals that the latter also possesses this property and is fully abstract.

(20) Bob Rosebrugh (Mount Allison, Canada)
"Tangled circuits"

This is a preliminary report. The bicategory of spans of graphs has been studied as an algebra of processes. The algebra captures many aspects of combining simple components to create complex systems. However it contains no account of "crossing wires". Using an augmentation of the braided monoidal category of tangles (freyd-Yetter) we can now describe circuits built from components and include information on the crossings of the wires joining components. We begin by an account in the simpler case of relations and extend to spans of sets.

(joint with N. Sabadini and RFC Walters)

"Convenient vector spaces, convenient manifolds and differential linear logic"

(slides here)

It was recently shown that the category of convenient vector spaces is a model of differential linear logic. Convenient vector spaces have sufficient structure to define a notion of smooth map, even though there are infinite-dimensional such spaces. A next logical step is to develop a theory of manifolds from the linear logic perspective.
There is a well-developed notion of convenient manifold, which reveals much additional structure not present in finite dimensions. We will examine this structure, and try to lift it to more general settings.

(22) Peter LeFanu Lumsdaine (Halifax, Canada)

"Higher inductive types: the circle and friends, axiomatically."
(Slides here)

The emerging field of “homotopy type theory” investigates logical systems whose primitive objects behave not like sets, but more like spaces or homotopy types — starting from the observation that familiar theories, such as intensional Martin-Löf type theory and the Calculus of Constructions, are already quite suitable.
A crucial type-constructor in such theories is inductive families. This allows definitions of such diverse types as dependent sums, identity types, booleans, and natural numbers, to be given very naturally as instances of a single general form.
I will discuss a further strengthening of this principle, to so-called higher inductive families. By allowing constructors to produce paths in a type (aka propositional equalities) as well as points in the type itself, one obtains type-theoretically natural definitions of many important spaces and topological constructions: the circle, higher-dimensional spheres, mapping cylinders, π₀ of any space…
(This covers some similar ground to my talk at the CMS meeting a week earlier, but I will try to keep the overlap in content minimal for the sake of repeat listeners.)

(23) Laura Scull (Fort Lewis, USA)

"What is half a point? An introduction to moduli spaces, orbifolds and groupoids"

Moduli spaces are widely used in physics and algebraic geometry for describing families of objects. In order to properly encode this information, however, the 'space' needs to have more structure than an ordinary space. This leads us to the world of orbifolds. In this talk, I will use an elementary example to motivate the need for this extra structure, and explain the geometry of orbifolds and how they can be described using the category theoretical language of groupoids. There will be lots of pictures and not many theorems; this will be the motivation for the work described by Dorette.

(24) Michele Pagini (Paris, France)

"The Computational Meaning of Probabilistic Coherence Spaces"

(Slides here)

We study probabilistic coherence spaces -- a denotational semantics interpreting programs by power series with non-negative real coefficients.  We prove that this semantics is adequate for a probabilistic extension of the untyped lambda-calculus: the probability that a term reduces to a head normal form is equal to its denotation computed on a suitable set of values.  The result gives, in a probabilistic setting, a quantitative refinement to the adequacy of Scott's model for untyped lambda calculus.

(26) Robert Dawson (St Mary's, Canada)

"Investigating computability in Turing categories"

(slides here)

The concept of a computable function between natural numbers is quite a habitual one, however, it is possible to capture certain important properties of computability in a special type of category, called a Turing category, at the heart of which there is a combinatory complete structure called a partial combinatory algebra (PCA). In this talk, I will give a brief overview of Turing categories, followed by a study of additional categorical structure they may contain, such as a range operator and coproducts, and how this is reflected in the underlying PCA.

Let D denote the downset monad on the category Pre of preorders and suppose T is a submonad of D. Then T induces a notion of compactness suitable for any sup-lattice. The taking of compact elements forms one half of an adjunction between T-algebras and a natural subcategory of Sup. Restriction to an equivalence between a category of posets and a category of frames yeilds a stone-type duality. We will explore a family examples in detail which permits a nice description of the resulting categories of posets and frames.

This is joint work with Pieter Hofstra and Dion Coumans and based on a paper of Olivia Caramello ("A topos-theoretic approach to Stone-type dualities" available on the arxive).

(29) Flavien Breuvart (ENS Cachan, France)

"Lambda Calculus with Test, full abstraction in D"

(slides here)

The full abstraction of the lambda calculus (or equivalently H*) into D has been proven by Wadsworth in 1976, but the proof itself was quite technical and syntactic and no fundamentally different proof has been found since then. The main point of this talk is to furnish a more semantic proof of this result with a totally new method that consists of extending a calculus with operations that conserve the same operational equivalence (on its restriction) but where we can observe the definability of D.
(30) Etienne Duchesne (Marseille, France)

"Geometry of interaction and uniformity"

(slides here)

We present a denotational semantics based on the geometry of interaction. We are particularly interested in the notion of uniformity which allows to handle exponentials; we define it by means of group invariance as in the orbital games of Melliès. Time permitting, an interpretation of polymorphism and the construction of a category of orthognality for MLL will be brefly presented, and we will discuss its extension to other fragments of linear logic.