Last Update: 2011-05-23.
For updates or additions to this page, please send a note to Robin Cockett.
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)
"Unifying notions of monadic strength"
(3) Robert Seely (McGill, Canada)
"Linear Functors and Modal
Logic"
(slides here)
(4) Dorette Pronk (Dalhousie, Canada)
"Atlas groupoids and
categories of fractions"
(5) Pieter Hofstra (Ottawa, Canada)
(6) Brett Giles (Calgary, Canada)
"Coproduct in inverse
categories"
(7) Jonathan Gallagher (Calgary, Canada)
"Differential Turing
categories"
(8) Geoff Cruttwell (Ottawa, Canada)
"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.
(9) Brian Redmond (Calgary, Canada)
(10) Robin Cockett (Calgary, Canada)
(11) Xuizhan Guo (Calgary, Canada)
(12) Pavel Hrubes (Calgary, Canada)
"On the Total Maps of a Turing
Category"
(13) Subashis Chakraborty (Calgary, Canada)
(14) Masuka Yeasin (Calgary, Canada)
(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
B→D
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 2→B
is exponentiable in Top. Since every functor 2→B
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.
(19) Guilio Manzonetto (Radboud, Netherlands)
"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)
(21) Rick Blute (Ottawa, Canada)
"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.
(25) Sebastian Lindner (Calgary, Canada)
(26) Robert Dawson (St Mary's, Canada)
(27) Polina Vinogradova (Ottawa, 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.
(28) Trevor Wares (Ottawa, Canada)
"Stone-Type Dualities
Generated by subMonads of the Downset Monad."
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.
Last Update: 2011-05-23.
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
2011.