Last Update: 2014-03-20. For updates
or additions to this page, please send a note to Robin
Cockett.
Attendees and Abstracts
(1) Robert Seely (McGill, Canada)
(Slides here)
Title: Revisiting the term calculus for BCST style proof-nets
(2) Pieter Hofstra (Ottawa, Canada)
Title: Isotropy theory, categorically
Abstract:
Given an action of a group on a set, we may consider the subgroup
consisting of those elements which fix a given element; this is
called the isotropy subgroup at that element. Similar ideas occur in
the theory of inverse semigroups, and topological groupoids. In this
tutorial, I will introduce a very general category-theoretic concept
of isotropy which captures these examples. In particular, I will
explain what isotropy of a small category is, and more generally
what the isotropy group of a Grothendieck topos (generalized space)
looks like. Time permitting, we will look at higher-order isotropy
as well.
(3) Brett Giles (Calgary, Canada)
Title: Inverse sums in inverse categories
Abstract:
Restriction categories as described by Cockett and Lack provide us
with an algebraic axiomatization of partiality in a category.
Inverse categories are restriction categories in which each map has
a partial inverse. In such a category, requiring that the category
has products or co-products forces the inverse category to have a
rather simple structure.
In this talk we will describe the addition of a construct called an
"inverse sum". An inverse sum is intended to provide much of the
richness of a co-product, without forcing the category to become
trivial. We will show how the inverse sum allows us to describe
disjointness of maps, disjoint joins and an inverse sum tensor.
Additionally we will show how an inverse category, with an inverse
sum tensor, is equivalent to a certain matrix category.
This is part of an ongoing research program to describe reversible
computing categorically and link that description to categorical
descriptions of standard computing.
(4) Geoff Cruttwell (Ottawa, Canada)
Title: Introducing
tangent categories
Abstract: This talk
will give a brief introduction to two categorical structures -
Cartesian differential categories and tangent categories.
Both arose out of a desire to give an axiomatic foundation for
settings in which an operation resembling differentiation
exists. I'll describe the relationship between these two
structures and view them both through the guiding example of the
category of smooth maps between powers of R.
Title: An alternative
view of the tangent category axioms
Abstract: Tangent
categories, first described by Rosicky, encompass a variety of
concrete settings for differential geometry. Recent work
has shown that much of the theory of differential geometry - for
example, vector fields, the Lie bracket, vector bundles, and
connections - can be developed in this abstract setting.
However, the axioms of a tangent category can seem quite
ad-hoc. They involve not only an endofunctor on the
category (representing the tangent bundle) but a number of
natural transformations with non-obvious properties.
In this talk, I'll
describe an alternative viewpoint for these axioms. I'll
show how the axioms for a tangent category can be seen as
intuitive refinements of a much simpler structure (a category
with an endofunctor and a natural transformation to the
identity). As a consequence, I'll describe what tangent
categories ``without addition'' would look like.
(5) Rory Lucyshyn-Wright (Ottawa, Canada)
Title: Categories with representable tangent structure and models of
SDG associated to codifferential categories
Abstract:
We show that every suitable codifferential category in the sense of
Blute-Cockett-Seely gives rise to a category with representable
tangent structure in the sense of Rosick\'y and Cockett-Cruttwell
and, under an additional hypothesis, a model of synthetic
differential geometry. Given any suitable codifferential
category (C,T,d), so that T is a given monad on C, we show that an
associated "Weil T-algebra" W(1) serves as an infinitesimal object D
(in the sense of Cockett-Cruttwell) in the opposite Aff_T :=
(C^T)^{op} of the category of T-algebras. For example, when C
is the category of K-modules for a commutative ring K and T is the
symmetric K-algebra monad on C, W(1) is the K-algebra of dual
numbers K[x]/(x^2) and Aff_T is the category of affine K-schemes. In
general, letting K be the monoidal unit of C, the infinitesimal
object D is a subobject of the "affine T-line" R = Spec(TK) in Aff_T
and consists of square-zero elements. The object D is exponentiable
in Aff_T, and the formal Kock-Lawvere axiom R x R \cong R^D holds.
Under an additional hypothesis, D consists of exactly the
square-zero elements of R, so that R is a ring of line type in Aff_T
and gives rise to a model of synthetic differential geometry. We
employ a novel theory of derivations in codifferential categories
recently developed in joint work of Blute, Lucyshyn-Wright, and
O'Neill.
(6) Aurore Alcolie (Lyon, France)
(Slides here)
Title: Cartesian closed 2-categories and rewriting
(7) Darien DeWolf (Dalhousie, Canada)
(Slides here)
Title:
On double inverse semigroups
Abstract:
In his book, "The Theory of Inverse Semigroups", Mark Lawson
describes two constructions from inverse semigroups to inductive
groupoids and back again. These constructions turn out to be
functorial and induce an isomorphism of categories. We extend these
constructions to double inverse semigroups and double inductive
groupoids -- all to be defined -- and show these constructions also
determine an isomorphism of categories. We use this isomorphism to
study the structure of double inverse semigroups.
(8) Bob Rosebrugh (Mount Allison, Canada)
(slides here)
Title: Asymmetric lenses, symmetric lenses, and spans
Abstract: What we now call "asymmetric lenses" were introduced about
ten years ago to provide strategies for the database "view
update problem": suppose y is a (view) state derived as y=gx for a
view g: X -> Y on database states X. When can an update
from y to another state y' be correctly propagated to an update x to
x'? There are several kinds of lenses depending on the
database state model.
Now suppose x and y are states from model spaces X and Y and are
known to be "synchronized" as witnessed by an (external) c.
How should an update to either of the states, say from x to x', be
correctly propagated to an update of the other state, say from Y to
y' with a resynchronization of the update state by some c'? To
adress this problem recent studies consider kinds of "symmetric"
lenses.
Both asymmetric and symmetric lenses and (equivalence classes of )
symmetric lenses of the various kinds are arrows of suitable
categories. We sketch these developments and show how
symmetric lenses can be generated from asymmetric lenses using the
span construction.
This is joint work with Mike Johnson.
(9) Poon Lueng (Macquarie University, Australia)
(Slides here)
Title: The Free Tangent structure
Abstract:
There has been much recent work into generalizing the structures
involved in the study of differential geometry. One approach,
which has been very influential, is synthetic differential geometry.
Another, due to Rosicky, focused more directly on the tangent
functor and its structure of (abelian) group bundle. More
recently, a further generalisation has been given by Cockett and
Cruttwell, detailing a structure involving the use of additive
bundles (commutative monoids). This type of structure in fact is
compatible with many existing definitions of differentiability,
including those used in computer science and combinatorics, the
manifolds in differential and algebraic geometry and also the
abstract definitions in synthetic differential geometry.
These tangent structures may be defined by giving an underlying
category and tangent functor with natural transformations satisfying
a set of axioms. My work looks at giving an alternative; namely that
these ideas of tangent structure can be captured by certain Weil
algebras and the morphisms between them. We ultimately aim to
show that the resulting category of Weil algebras has tangent
structure which is universal with respect to any category equipped
with such structure.
(10) Prashant Kumar (Calgary, Canada)
(Slides here)
Title: A brief survey of some abstract machines
(11) Chad Nestor (Calgary, Canada)
(slides here)
Title: Turing categories and incompleteness
(12) Keith O'Neill (Ottawa, Canada)
Title: Universal Derivations in Codifferential Categories
Abstract: In this joint work with Richard Blute and Rory
Lucyshyn-Wright, we present structural results about
\emph{codifferential categories} as defined in
Blute-Cockett-Seely. Namely, it is shown that under modest
hypotheses, every codifferential category is a \emph{K\"ahler
category} as defined in Blute-Cockett-Porter-Seely. The proof of
this fact is in striking contrast to that of the similar,
conditional result in Blute-Cockett-Porter-Seely. The difference is
reconciled by a novel notion of derivation for codifferential
categories, with which the universal derivations of a codifferential
category are shown to accord with those which were proposed in
Blute-Cockett-Porter-Seely.
(13) John Macdonald (UBC, Canada)
(14) Dorette Pronk (Dalhousie, Canada)
(Slides here)
Title: Orbifolds as manifolds
Abstract:
I will describe a join restriction category of charts and maps
defined in terms of topological profunctors, and then apply the
manifold construction to obtain orbifolds.
This is joint work with Laura Scull.
(15) Robin Cockett (Calgary, Canada)
(16) Kristine Bauer (Calgary, Canada)
Title: Working towards Andr\'e-Quillen homology
Abstract:
Almost 50 years ago, M. Andr\'e and D. Quillen independently
discovered a homology theory theory for commutative rings. The
homology theory arises as a derived functor of the derivations
functor and it is used extensively in commutative algebra.
About a decade ago, M.R. Kantorvicz and R. McCarthy founs that
Andre-Quillen homology could be recovered as the first derivative of
a particular functor using Goodwillie's calculus of functors.
However, their construction required artificially adding a base
point (an object which is both initial and final). B. Johnson,
R. McCarthy and I have extended the kind of fuctor calculus used in
that calculation so there is no longer a requirement for a
basepoint. One ought to be able to express
Andre-Quillen homology as the first derivative of a functor again,
but this time without adding a basepoint. This was the goal of
a workshop last summer, and it is work in progress by myself, M.
Basterra, A. Beaudry, R. Eldred, B. Johnson, M. Merling, and S.
Yeakel. I will discuss our progress towards this result.
(17) Robin Houston (Manchester, UK)
(Slides here)
Title: No proof nets for MLL with units
MLL proof equivalence is the problem of deciding whether two proofs
in multiplicative linear logic are equivalent up to permutations. It
is also, equivalently, the word problem for ∗-autonomous categories.
Previous work has shown the problem to be equivalent to a rewiring
problem on proof nets, which are not canonical for full MLL due to
the presence of the two units. I’ll show that MLL proof equivalence
is PSPACE-complete, using a reduction from Hearn and Demaine’s
Nondeterministic Constraint Logic. An important consequence of the
result is that the existence of a satisfactory notion of proof nets
for MLL with units is ruled out (under current complexity
assumptions).
In the first session I’ll give an overview of the problem, and the
reduction strategy, and try to give some intuition for the dynamics
of the equivalence relation. In the second I’ll explain the
construction in more detail, with the aim of at least making it
reasonable for the audience to believe that the reduction works as
claimed.
A reasonably complete account of the construction and proof is
available here .
(18) Simon Fortier-Garcceau (Ottawa, Canada)
(slides here)
Title: An Introduction to the object-oriented calculus
Abstract:
We are quite familiar with the lambda calculus that serves as
a theoretical basis for the functional programming
paradigm. There are three other major programming paradigms,
one of which is object-oriented programming (OOP).
OOP is the most popular programming paradigm in the software
engineering world today as it is a natural, intuitive and powerful
approach to the development of software. It has mathematical
foundations in the same way as the functional programming paradigm
has; that is there is a theory of objects, the sigma-calculus, which
was developed by Luca Cardelli and Martin Abadi over the
1990s. This theory reflects, at a deeper level, the modelling
issues that an object oriented programmer encounters in practice,
and as such it is an important theory in the study of computer
science.
The goal of this talk will be to explore the syntax and semantics of
the first-order theory of objects. In particular, we will
investigate the subtyping of objects and polymorphism, and the
important theoretical problem of multiple inheritance in 00P, and
why it is an active field of research.
(19) Christopher Dutchyn (Saskatewan, Canada)
(20) Hugo Bacard (University of Western Ontario)
Title: Strictification of co-Segal dg-categories
Abstract:
Given a monoidal category {\cal M} = (M,\ox,I) we develop a theory
of homotopy enriched categories with the notion of co-Segal
enriched category. Our motivation for this theory is
when {\cal M} is a category of chain complexes, in which case we
have what we call co-Segal dg-categories.
In this talk I will describe the model structure on co-Segal
dg-categories and show it has better properties than the model
structure on strict dg-categories. I will also show that and
co-Segal dg-category is weakly equivalent to a strict
dg-category. These results hold for any symmetric
monoidal category {\cal M} (M \ox,I) whose underlying model category
M is combinatorial.
(21) Robert Dawson (St Mary's University, Canada)
(22) Mike Pors (Calgary, Canada)
(Slides here)
Title: Hurewicz for Symmetric Spectra
In sufficiently nice
categories of topological spaces (CW-complexes, compactly
generated weak Hausdorff spaces, simplicial complexes, etc)
There are two nice functors called the homotopy
groups and the
homology groups respectively which, conceptually,
measure the number and type of holes in a given space. These
functors, and variants of them, are the main objects of study in
algebraic topology. There is a natural transformation between
these called the hurewicz
map which eases computation of these functors in some
cases. All of this has been known for nearly 100 years now.
More recently, a nice
extension of the category of `nice' topological spaces onto
which the homotopy and homology functors extend has been brought
to light by Hovey, Shipley, and Smith. In this talk I will
provide an introduction to this category (the objects of which
are called symmetric
spectra, the extensions of homotopy and homology to this
category, and the hurewicz map between them.
(23) Phil Mulry (Colgate, USA)
(24) Adam Gerlings (Calgary, Canada)
(Slides here)
Title: Categorical aspects of Galois theory
Abstract: The notion of a Galois category was first introduced by
Grothendieck while studying coverings of schemes in algebraic
geometry. These categories can be characterized by a list of axioms,
as was done by Grothendieck, and revisited by numerous other authors
over the years. However, study into the structure behind these
Galois categories has been minimal. Recent work by Cockett has shown
a new, purely categorical, method for describing Galois categories,
and doing so at a higher level of understanding. In this talk, I
will describe the Grothendieck view of a Galois category and the
newer, categorical approach.
(25) Jonathan Gallagher (Calgary, Canada)
Last
Update: 2014-03-20. For updates or additions to this
page, please send a note to
Robin
Cockett.
Back to the main page for Foundational
Methods in Computer Science 2014.