Participants:
(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.
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.
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.
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.
Jeff Egger (Edinburgh,UK)
"Strict negaion in cyclic and arbitrary
*-autonomous categories"
(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.
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.
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.
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.
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)
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.
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.
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)
"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.
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.
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.
Robin Cockett (Calgary, Canada)
"Integral categories"
Xuizhan Guo (Calgary, Canada)*
"On the free meet and product
completions of restriction categories"
James King (Calgary, Canada)