(Photos by Brett Giles here)

Simona Paoli (Penn State Altoona, USA)

"Cohomology of track categories"

Track categories are 2-categories with invertible 2-cells. They appear in a variety of contexts in category theory as well as in homotopy theory. in this talk we discuss a cohomology theory of track categories. We give different constructions of this cohomology: in terms of a classically defined cohomology of simplicial enriched categories, in terms of a new type of complex built usiing Street's nerve of the track category. and in terms of a Barr-Beck-Quillen approach. We discuss the relevance of this cohomology to giving algebraic and categorical descriptions of the k-invariants in the second Postnikov decompositions of a simplicially enriched category. This is joint work with David Blanc.

Track categories are 2-categories with invertible 2-cells. They appear in a variety of contexts in category theory as well as in homotopy theory. in this talk we discuss a cohomology theory of track categories. We give different constructions of this cohomology: in terms of a classically defined cohomology of simplicial enriched categories, in terms of a new type of complex built usiing Street's nerve of the track category. and in terms of a Barr-Beck-Quillen approach. We discuss the relevance of this cohomology to giving algebraic and categorical descriptions of the k-invariants in the second Postnikov decompositions of a simplicially enriched category. This is joint work with David Blanc.

Lionel Vaux (Universite de la Mediterranee, France)

"Web based models of linear
logic" (Tutorial talks)

Pierre Clairambault (Paris, France)

"Strong functors and interleaving fixed
points in game semantics"

In this talk, I will prent a sequent calculus \muLJ with induction and coinduction, at the intersection of the \mu-calculus and the intuitionistic sequent calculus LJ and i will show how HO game semantics and parity winning conditions can be combined to give a precise denotational model for it. I will first describe this model for a "weak" fragment of \muLJ, where one can only iterate closed terms. Extending the model to the full rule set of \muLJ requires one to prove that open types are interpreted as strong functors, and to examine how initial algebras and terminal algebras are preserved by functorial liftings. Following these ides, I will show how to extend the above games model for the full rule set of \muLJ.

In this talk, I will prent a sequent calculus \muLJ with induction and coinduction, at the intersection of the \mu-calculus and the intuitionistic sequent calculus LJ and i will show how HO game semantics and parity winning conditions can be combined to give a precise denotational model for it. I will first describe this model for a "weak" fragment of \muLJ, where one can only iterate closed terms. Extending the model to the full rule set of \muLJ requires one to prove that open types are interpreted as strong functors, and to examine how initial algebras and terminal algebras are preserved by functorial liftings. Following these ides, I will show how to extend the above games model for the full rule set of \muLJ.

Marc Bagnol (ENS, France)

"Towards a quantum model of linear
logics"

I will present the basics of "Quantum Coherence Spaces" (QCS), based on J.-Y. Girard's construction [paper] with slight --though important-- modifications. QCS is intended to become a model of linear logics, as a generalised version of coherence spaces in a world of matrices and operators, based on physical intuitions. Although the modelling of multiplicative connectives is exactly what we expect, we will see that the additives connectives turn out to be more tricky. This is related with eta-expansion and indeed one of the most interesting features of the model.

I will present the basics of "Quantum Coherence Spaces" (QCS), based on J.-Y. Girard's construction [paper] with slight --though important-- modifications. QCS is intended to become a model of linear logics, as a generalised version of coherence spaces in a world of matrices and operators, based on physical intuitions. Although the modelling of multiplicative connectives is exactly what we expect, we will see that the additives connectives turn out to be more tricky. This is related with eta-expansion and indeed one of the most interesting features of the model.

Micah McCurdy (Maquarie, Aus)

"V-Prof" (Joint work with Jeff Egger)

Fix a monoidal category V. We consider the question: What conditions are required on V to form the category of V-enriched profunctors, and what else must we demand of V so as to make V-Prof a cyclic linearly distributive category, or, indeed, cyclic star-autonomous? Guided by the example of Kimmo Rosenthal, who considered the endo-profunctors of a single V-category, for V symmetric star-autonomous, we will first consider endo-profunctors and proceed from there.

Fix a monoidal category V. We consider the question: What conditions are required on V to form the category of V-enriched profunctors, and what else must we demand of V so as to make V-Prof a cyclic linearly distributive category, or, indeed, cyclic star-autonomous? Guided by the example of Kimmo Rosenthal, who considered the endo-profunctors of a single V-category, for V symmetric star-autonomous, we will first consider endo-profunctors and proceed from there.

Jeff Egger (Edinburgh,UK)

"Strict negaion in cyclic and arbitrary
*-autonomous categories"

(Joint work with Micah McCurdy)

(Joint work with Micah McCurdy)

Vaughan Pratt (Stanford, USA)

"Topologogical algebra based on sorts
and properties of free and cofree structures"

Working within an arbitrary category of universes and their maps, we arbitrarily nominate certain universes as free and other as cofree. Leaving all four of these kind of entities undefined we give criteria by which certain of them are judged to be sorts, elements, variables, terms, operations, properties, open sets, and dependencies between properties.

Our main theorem is that every map is both homomorphic and continuous in the usual sense. With additional assumptions of extensionality and maximality we show that the category is equivalent to the category of all topological algebras and continuous homomorphisms between them for some signature and some axioms.

This framework extends topology to universal topology in a manner dual to how group theory extends to multisorted universal algebra, with properties dual to sorts. Dependencies of properties on each other arise as the dual of operations between sorts, and act on states in the same way operations act on elements. We show that operations dependencies, and maps act independently in the sense of commuting with each other. this framework permits both ordinary topological spaces and pointless locales to be readily defined, using one free and one cofree universe for the former and no free universe and one cofree universe per ordinal for the other.

The framework shed light on the long-standing philosophical question, can properties have extensions analogous to the extensions of a sort as the set of individulas of that sort, which we answer by taking the extension of a property to be the form of a Kripke structure whose worlds specialize in that property. It also provides a natural positive answer to the more recent and hotly debated question, do qualia exist. By allowing qualia of sort s for a property p, for example the taste of a wine, to be defined schizophrenically as either a material element of a cofree universe K_p or information about a free universe F_s ... one can become a qualophile.

Working within an arbitrary category of universes and their maps, we arbitrarily nominate certain universes as free and other as cofree. Leaving all four of these kind of entities undefined we give criteria by which certain of them are judged to be sorts, elements, variables, terms, operations, properties, open sets, and dependencies between properties.

Our main theorem is that every map is both homomorphic and continuous in the usual sense. With additional assumptions of extensionality and maximality we show that the category is equivalent to the category of all topological algebras and continuous homomorphisms between them for some signature and some axioms.

This framework extends topology to universal topology in a manner dual to how group theory extends to multisorted universal algebra, with properties dual to sorts. Dependencies of properties on each other arise as the dual of operations between sorts, and act on states in the same way operations act on elements. We show that operations dependencies, and maps act independently in the sense of commuting with each other. this framework permits both ordinary topological spaces and pointless locales to be readily defined, using one free and one cofree universe for the former and no free universe and one cofree universe per ordinal for the other.

The framework shed light on the long-standing philosophical question, can properties have extensions analogous to the extensions of a sort as the set of individulas of that sort, which we answer by taking the extension of a property to be the form of a Kripke structure whose worlds specialize in that property. It also provides a natural positive answer to the more recent and hotly debated question, do qualia exist. By allowing qualia of sort s for a property p, for example the taste of a wine, to be defined schizophrenically as either a material element of a cofree universe K_p or information about a free universe F_s ... one can become a qualophile.

Ernie Manes (UMass, USA)

"Cauchy sequences and Euclidean
Geometry:
a foundational method in computing"

Phil Mulry (Colgate, USA)

David Spivak (USA)

"Simplicial Databases"

I'll discuss a category-theoretic model
of databases in which a schema
is a labeled simplicial set X and data is represented as a sheaf over
X. Given a schema, the category of database states over it is a
boolean topos, and a morphism of schema induces a geometric morphism of
toposes. Moreover, limits and colimits represent joins, selects,
unions, and insertions of data.

Art Stone (BC,Canada)Robert Seely (McGill, Canada)

"Faa di Bruno categories"

For Cartesian differential categories the chain rule is a consequence of the composition in the "bundle category" which is a simple fibration.

This talk generalizes this situation using the higher-order chain rules originally developed by Faa Di Bruno in the nineteenth century, to produce a fibration Faa(\X) -> \X which is, in fact, the counit of a comonad on the category of left additive categories. Cartesian differential categories then arise precisely as coalgebras of this comonad.

For Cartesian differential categories the chain rule is a consequence of the composition in the "bundle category" which is a simple fibration.

This talk generalizes this situation using the higher-order chain rules originally developed by Faa Di Bruno in the nineteenth century, to produce a fibration Faa(\X) -> \X which is, in fact, the counit of a comonad on the category of left additive categories. Cartesian differential categories then arise precisely as coalgebras of this comonad.

Dorette Pronk (Dalhousie, Canada)

"Lie Groupoids, Morita
Equivalence, and Orbifold Homotopy Theory"

Abstract: In this talk I will discuss the representation of orbifolds by proper foliation groupoids (that is, Lie groupoids with a proper diagonal and discrete isotropy groups). By considering the corresponding toposes of equivariant sheaves we obtain the bicategory of orbifolds as a bicategory of fractions of the 2-category of proper foliation groupoids with respect to essential equivalences. This leads us to a notion of Morita equivalence for such groupoids.

Abstract: In this talk I will discuss the representation of orbifolds by proper foliation groupoids (that is, Lie groupoids with a proper diagonal and discrete isotropy groups). By considering the corresponding toposes of equivariant sheaves we obtain the bicategory of orbifolds as a bicategory of fractions of the 2-category of proper foliation groupoids with respect to essential equivalences. This leads us to a notion of Morita equivalence for such groupoids.

Pieter Hofstra (Ottawa, Canada)

"What is a linear combinatory algebra"

Lambda calculus and combinatory logic play a fundamental role in the theory of computing. The models of these theories (called lambda algebras and combinatory algebras respectively) generate categorical settings in which one may develop elementary recursion theory in a purely categorical fashion. In the case of lambda algebras, these categories are cartesian closed, while in the case of combinatory logic they have finite products but are only closed in a weak sense.

One may relax the notion of a combinatory algebra in several ways to obtain weaker notions of computation. For example, Martin Hofmann used so-called BCK algebras in his study of P-time computability. And Abramsky, Haghverdi, and Scott identified a notion of linear combinatory algebra, arising from traced monoidal categories and the axiomatic setting for the Geometry of Interaction programme.

In this talk I will give a brief introduction to the theory of standard combinatory algebras and the categories associated to these. Then I will consider various weakenings and refinements, identifying a very general notion of linear combinatory algebra in a monoidal category. Next, I will discuss the extent to which these structures generate interesting categorical structures, and finally I will look at the interaction with exponential comonads.

Lambda calculus and combinatory logic play a fundamental role in the theory of computing. The models of these theories (called lambda algebras and combinatory algebras respectively) generate categorical settings in which one may develop elementary recursion theory in a purely categorical fashion. In the case of lambda algebras, these categories are cartesian closed, while in the case of combinatory logic they have finite products but are only closed in a weak sense.

One may relax the notion of a combinatory algebra in several ways to obtain weaker notions of computation. For example, Martin Hofmann used so-called BCK algebras in his study of P-time computability. And Abramsky, Haghverdi, and Scott identified a notion of linear combinatory algebra, arising from traced monoidal categories and the axiomatic setting for the Geometry of Interaction programme.

In this talk I will give a brief introduction to the theory of standard combinatory algebras and the categories associated to these. Then I will consider various weakenings and refinements, identifying a very general notion of linear combinatory algebra in a monoidal category. Next, I will discuss the extent to which these structures generate interesting categorical structures, and finally I will look at the interaction with exponential comonads.

Phil Scott (Ottawa, Canada)

"Towards polarized GoI"

Octavio Malherbe (Ottawa, Canada)

"Partially traced categories and
paracategories"

We consider Freyd's notion of a paracategory and we prove that every partially traced category, in the sense of Haghverdi and Scott, can be faithfully embedded in a symmetric monoidal compact category.

Emily Diepenveen (Ottawa, Canada)We consider Freyd's notion of a paracategory and we prove that every partially traced category, in the sense of Haghverdi and Scott, can be faithfully embedded in a symmetric monoidal compact category.

Trevor Wares (Ottawa, Canada)

"Brouwer's principle of higher order
Heyting arithmetic"

Brouwer's principle is the statement that all total functions between the reals are continuous. While obviously not true this is a theorem of Brouwer's within his (informal) intuitionistic setting. In a formal setting this principe can be stated as a theorem, or as a derived rule of inference. We consider the latter in for higher order Heyting arithmetic - the former does not hold.

The proof uses Topos theory: we shall introduce the internal languiage of a Topos, say what we mean by the real numbers, and sketch the proof that Brouwer's principle holds.

Brouwer's principle is the statement that all total functions between the reals are continuous. While obviously not true this is a theorem of Brouwer's within his (informal) intuitionistic setting. In a formal setting this principe can be stated as a theorem, or as a derived rule of inference. We consider the latter in for higher order Heyting arithmetic - the former does not hold.

The proof uses Topos theory: we shall introduce the internal languiage of a Topos, say what we mean by the real numbers, and sketch the proof that Brouwer's principle holds.

Mike Burrell (Western, Canada)

"Inferring bounds for Pola"

Pola is a programming language in which every well-types program halts in polynomial time. This allows the potential for the compiler to statically and automatically infer bounds for Pola program -- most importantly time bounds. We discuss the implementation details in modelling and inferring bounds for Pola programs which can be tight enough for practical use.

Pola is a programming language in which every well-types program halts in polynomial time. This allows the potential for the compiler to statically and automatically infer bounds for Pola program -- most importantly time bounds. We discuss the implementation details in modelling and inferring bounds for Pola programs which can be tight enough for practical use.

Brett Giles (Calgary, Canada)

"Quantum programming and its semantics"

I will introduce LQPL (a Linear Quantum programming Language) and discuss its operational semanics. LQPL is based on the description of Quantum programming, using a C-like syntax introduced by Peter Selinger. LQPL has algebraic data types, recursive functions, some basic unitary transformations, and a limited classical processing facilities. The compiler enforces type safety and execution path balancing and translates programs into code for a Quantum stack machine: the emulator provides a visualization of a "Quantum stack". I will demonstrate how the language can be used to implement some simple Quantum and probabilistic algorithms. I will conclude by discussing some of Landry Huet work on the semantics of simple algebraic data types in the Quantum setting.

Jonathan Gallager (Calgary, Canada)I will introduce LQPL (a Linear Quantum programming Language) and discuss its operational semanics. LQPL is based on the description of Quantum programming, using a C-like syntax introduced by Peter Selinger. LQPL has algebraic data types, recursive functions, some basic unitary transformations, and a limited classical processing facilities. The compiler enforces type safety and execution path balancing and translates programs into code for a Quantum stack machine: the emulator provides a visualization of a "Quantum stack". I will demonstrate how the language can be used to implement some simple Quantum and probabilistic algorithms. I will conclude by discussing some of Landry Huet work on the semantics of simple algebraic data types in the Quantum setting.

"Differential restriction categories I"

This talk will present differential restriction categories and their development from (cartesian) differential categories. In particular, the axioms of differential restriction categories will be given, while pointing out the differences from the basic total notion. Two examples of differential restriction categories will be developed to illustrate the axiomatization: smooth functions on open subsets of $\mathbb{R}^n$ and rational functions over a commutative ring.

This talk will present differential restriction categories and their development from (cartesian) differential categories. In particular, the axioms of differential restriction categories will be given, while pointing out the differences from the basic total notion. Two examples of differential restriction categories will be developed to illustrate the axiomatization: smooth functions on open subsets of $\mathbb{R}^n$ and rational functions over a commutative ring.

Geoff Cruttwell (Calgary, Canada)

"Differential restriction categories II"

This talk will discuss some of the interesting issue which arise when combining restriction structure with differential structure. One issue which arises is the definition of "additive" and "linear" which are more subtle than their total version. Also I will show that when one join completes or classically complete a differential category the result has a differential restriction structure.

This talk will discuss some of the interesting issue which arise when combining restriction structure with differential structure. One issue which arises is the definition of "additive" and "linear" which are more subtle than their total version. Also I will show that when one join completes or classically complete a differential category the result has a differential restriction structure.

Brian Redmond (Calgary, Canada)

"A categorical tour of lower complexity"

I shall discuss the use of polarized strong categories as an abstract setting for investigating lower complexity computations and illustrate the theory with R-sized sets and polnomially bounded maps. Correponding type systems for both polynomial time (PTIME) and polynomial space (PSPACE) will be discussed and their separation explained by a distributive law (products over coproducts). Finally, if time permits, important complexity classes within PSPACE. for example non-deterministic polynomial time (NP) and the polynomial hierarchy (PH) will be discussed and interpreted within our PSPACE setting.

I shall discuss the use of polarized strong categories as an abstract setting for investigating lower complexity computations and illustrate the theory with R-sized sets and polnomially bounded maps. Correponding type systems for both polynomial time (PTIME) and polynomial space (PSPACE) will be discussed and their separation explained by a distributive law (products over coproducts). Finally, if time permits, important complexity classes within PSPACE. for example non-deterministic polynomial time (NP) and the polynomial hierarchy (PH) will be discussed and interpreted within our PSPACE setting.

Robin Cockett (Calgary, Canada)

"Integral categories"

Xuizhan Guo (Calgary, Canada)*

"On the free meet and product completions of restriction categories"

James King (Calgary, Canada)