 JOHN BAEZ, U. C. Riverside
Categories in Control [PDF]

Control theory is the branch of engineering that studies dynamical systems with inputs and outputs, and seeks to stabilize these using feedback. Control theory uses 'signalflow diagrams' to describe processes where realvalued functions of time are added, multiplied by scalars, differentiated and integrated, duplicated and deleted. In fact, these are string diagrams for the symmetric monoidal category of finitedimensional vector spaces and the monoidal structure is direct sum. Jason Erbele and I found a presentation for this symmetric monoidal category, which amounts to saying that it is the PROP for bicommutative bimonoids with some extra structure.
A broader class of signalflow diagrams also includes extra morphisms to model feedback. This amounts to working with the symmetric monoidal category where objects are finitedimensional vector spaces and the morphisms are linear relations. Erbele also found a presentation for this larger symmetric monoidal category. It is the PROP for a remarkable thing: roughly speaking, an object with two commutative Frobenius algebra structures, such that the multiplication and unit of either one and the comultiplication and counit of the other fit together to form a bimonoid.
In electrical engineering we also need a category where a morphism is a circuit made of resistors, inductors and capacitors. Brendan Fong and I proved there is a functor mapping any such circuit to the relation it imposes between currents and potentials at the inputs and outputs. This functor goes from the category of circuits to the category of finitedimensional vector spaces and linear relations.
 MARC BAGNOL, University of Ottawa
Proofnets and the Complexity of Proof Equivalence [PDF]

Also known as the word problem in category theory, the equivalence problem of a logic asks whether two proofs are related by a set of rule permutation that reflect the commutative conversions of the logic. On the other hand, proofnets for a logic can be broadly defined as combinatorial objects offering canonical representatives for equivalence classes of proofs, enjoying good computational properties.
A notion of proofnet for a logic therefore induces a way to solve the equivalence problem of this logic. This has been used recently to show that the multiplicative fragment (with units) of linear logic cannot have a lowcomplexity notion of proofnets, by proving that the equivalence problem for this fragment is PSpacecomplete.
We will look into the situation for another small fragment of linear logic: the multiplicativeadditive (without units) fragment, which intuitionistic part can be seen as a very basic linear $\lambda$calculus with coproducts.
 RICHARD BLUTE, University of Ottawa
Towards a Theory of Integral Linear Logic via RotaBaxter algebras [PDF]

Differential linear logic, as introduced by Ehrhard and Regnier, extends linear logic with an inference rule which is a
syntactic version of differentiation. The corresponding categorical structures, called differential categories, were
introduced by Blute, Cockett and Seely. Differential categories are monoidal categories equipped with a comonad
which endows objects in its image with a cocommutative coalgebra structure. There is also a natural transformation,
called the deriving transform, which models the differential inference rule. The large number of examples of differential categories demonstrate the utility of the idea. These include the convenient vector spaces of Frohlicher and Kriegl.
It is an ongoing project to develop similar notions of integral linear logic and integral categories. An appropriate place to draw inspiration for this is the theory of RotaBaxter algebras. RotaBaxter algebras are associative algebras with an
endomorphism which satisfies an abstraction of the integration by parts formula. There are many examples of such algebras and multiobject versions of these examples should provide important examples of models of integral linear logic.
 ANDREW CAVE, McGill
Linear temporal logic proofs as reactive programs [PDF]

In this talk I describe a constructive variant of linear temporal logic, and describe its interpretation as a reactive programming language via the propositionsastypes correspondence. The upshot is that the type discipline enforces causality and liveness properties of its programs. I will also discuss a variant system which realizes a version of the GödelLöb principle.
 FLORENCE CLERC, McGill
Presenting a Category Modulo a Rewriting System [PDF]

Presentations of categories is a useful tool to describe categories by the means of generators for objects and morphisms and relations on morphisms. However problems arise when trying to generalize this construction when objects are considered modulo an equivalence. Three different constructions can be used to describe such generalization : localization, quotient and considering only normal forms with respect to a certain rewriting system.
I will present some work done in collaboration with S.Mimram and P.L.Curien. We assume two kinds of hypotheses, namely convergence and cylinder property (which is some higherdimensional convergence). Under these assumptions, we prove that there is an equivalence of categories between the quotient and the localization, and an isomorphism of categories between the quotient and the category of normal forms.
 ROBIN COCKETT, University of Calgary
The Basics of Integral Categories [PDF]

Differential categories of both tensor and Cartesian stripes have been around for quite a while: what do the corresponding structures for integral categories look like?
The talk will describe integral categories and their relationship to differential categories. It will also describe the more general notion of an antiderivative (due to Ehrhard), how these arise in this context, and how they produce integration. Some models of integral categories will be described. If time permits, the Cartesian version of these notions will be discussed.
 JOSEE DESHARNAIS, Université Laval
Almost Sure Bisimulation in Labelled Markov Processes [PDF]

In this talk we propose a notion of bisimulation for labelled Markov processes parameterised by negligible sets (LMPns). The point is to allow us to say things like two LMPs are “almost surely” bisimilar when they are bisimilar everywhere except on a negligible set. Usually negligible sets are sets of measure 0, but we work with abstract ideals of negligible sets and so do not introduce an adhoc measure.
The construction is given in two steps. First a refined version of the category of measurable spaces is set up, where objects incorporate ideals of negligible subsets, and arrows are identified when they induce the same homomorphisms from their target to their source $\sigma$algebras up to negligible sets. Epis are characterised as arrows reflecting negligible subsets. Second, LMPns are obtained as coalgebras of a refined version of Giry’s probabilistic monad. This gives us the machinery to remove certain counterintuitive examples where systems were bisimilar except for a negligible set. Our new notion of bisimilarity is then defined using cospans of epis in the associated category of coalgebras, and is found to coincide with a suitable logical equivalence given by the LMP modal logic. This notion of bisimulation is given in full generality  not restricted to analytic spaces. The original theory is recovered by taking the empty set to be the only negligible set.
 NORM FERNS, York University
Bisimulation Through Markov Decision Process Coupling [PDF]

Markov decision processes (MDPs) are a popular mathematical model for sequential decisionmaking under uncertainty. Many standard solution methods are based on computing or learning the optimal value function, which reflects the expected return one can achieve in each state by choosing actions according to an optimal policy. In order to deal with large state spaces, one often turns to approximation.
Bisimulation metrics have been used to establish approximation bounds for state aggregation and other forms of value function approximation in MDPs. In this talk, we show that a bisimulation metric defined on the state space of an MDP in previous work can be viewed as the optimal value function of an optimal coupling of two copies of the original model, and discuss the consequences thereof.
This is joint work with Doina Precup.
 JÉRÔME FORTIER, Université d'Ottawa
Circular Proofs [PDF]

Selfreferential objects such as natural numbers, infinite words, languages accepted by abstract machines, finite and infinite trees and so on, live in the world of $\mu$bicomplete categories, where they arise from the following operations: finite products and coproducts, initial algebras (induction) and final coalgebras (coinduction). Circular proofs were introduced by Santocanale in order to provide a logical syntax for defining morphisms between such objects. We have indeed shown full completeness of circular proofs with respect to free $\mu$bicomplete categories. The main practical advantage of having such a syntax is that it provides a general evaluation algorithm, via a cutelimination procedure. We can then see circular proofs as a new kind of abstract machine, for which we will explore some computabilityrelated questions.
 PIETER HOFSTRA, University of Ottawa
Monads and Isotropy [PDF]

In joint work with Funk and Steinberg (``Isotropy and Crossed Toposes", TAC, 2012), a new algebraic invariant of Grothendieck toposes was introduced: just as every topos contains a canonical locale (its subobject classifier), it also contains a canonical group, called its \emph{isotropy group}. In this talk, I will survey some of the recent developments concerning isotropy groups of toposes and of small categories, and in particular explain how this gives rise to some new monads on the category of small categories, one of which can be viewed as encoding formal conjugation in a category.
 ANDRÉ JOYAL, UQAM
Simplicial tribes for homotopy type theory [PDF]

A tribe is a categorical model of homotopy type theory.
We would like to show that the category of tribes has the structure of a fibration category,
but path objects are missing.
To correct this, we introduce the notion of simplicial tribes.
 BRIGITTE PIENTKA, McGill University
Mechanizing MetaTheory in Beluga [PDF]

Mechanizing formal systems, given via axioms and inference rules,
together with proofs about them plays an important role in
establishing trust in formal developments. In this talk, I will
survey the proof environment Beluga. To specify formal systems and
represent derivations within them, Beluga provides a sophisticated
infrastructure based on the logical framework LF; to reason about formal
systems, Beluga provides a dependently typed functional language for
implementing inductive proofs about derivation trees as recursive functions
following the CurryHoward isomorphism. Key to this approach is the ability to
model derivation trees that depend on a context of assumptions using a
generalization of the logical framework LF, i.e. contextual LF which supports
firstclass contexts and simultaneous substitutions.
Our experience has demonstrated that Beluga enables direct and compact
mechanizations of the metatheory of formal systems, in particular programming
languages and logics. To demonstrate Beluga's strength in this talk, we develop
a weak normalization proof using logical relations.
 PHIL SCOTT, University of Ottawa
AF Inverse Monoids and the Coordinatization of MValgebras [PDF]

MValgebras are the algebras associated to manyvalued logics, analogous to the way that Boolean algebras are associated to classical propositional logics. In the mid1980's, D. Mundici established an equivalence between the category of MValgebras and the category of $\ell$groups (with archimedean order unit). This restricts to a correspondence between countable MValgebras and AF C*algebras with latticeordered $K_0$ group. We introduce a class of AF inverse Boolean
monoids and prove a coordinatization theorem (in the spirit of von Neumann's Continuous Geometry). This theorem states that every countable MValgebra can be coordinatized (i.e. is isomorphic to the
lattice of principal ideals of some AF Boolean inverse monoid). Techniques involve use of Bratteli diagrams and colimits of semisimple inverse monoids. We shall illustrate this in the case of certain
specific AF C*algebras (e.g. the CAR algebra of a Fermi gas). If time permits, we will mention related work, e.g. relations with Effect Algebras (B. Jacobs) and a general coordinatization theorem in recent work of F. Wehrung. [Joint work with Mark Lawson (HeriotWatt)]
 ROBERT SEELY, McGill University \& John Abbott College
Two categorical approaches to differentiation [PDF]

In the past decade, we (coauthors Rick Blute, Robin Cockett and I) have formulated two different abstract categorical approaches to differential calculus, based on the structure of linear logic (an idea of Ehrhard and Regnier). The basic idea has two types of maps (``analytic'' or ``smooth'', and ``linear''), a comonad $S$ (a ``coalgebra modality''), somewhat like the {\bf!} of linear logic, and a differentiation operator. In our first approach ({\bf monoidal differential categories}), the coKleisli category (the category of cofree coalgebras) of $S$ consists of smooth maps, and differentiation operates on coKleisli maps to smoothly produce linear maps. Our second approach ({\bf Cartesian differential categories}) reversed this orientation, directly characterizing the smooth maps and situating the linear maps as a subcategory. If $S$ is a ``storage modality'', meaning essentially that the ``exponential isomorphisms'' from linear logic ($S(X\times Y)\simeq S(X)\otimes S(Y)$ and $S(1)\simeq S(\top)$) hold, we get a tight connection between these approaches in the Cartesian (monoidal) closed cases: the linear maps of a Cartesian closed differential storage category form a monoidal closed differential storage category, and the coKleisli category of a monoidal closed differential storage category is a Cartesian closed differential storage category. Two technical aides in proving these results are the development of a graphical calculus as well as a term calculus for the maps of these categories. With the term calculus, one can construct arguments using a language similar to that of ordinary undergraduate calculus.
 PETER SELINGER, Dalhousie University
Numbertheoretic methods in quantum computing [PDF]

An important problem in quantum computation is the socalled
approximate synthesis problem: to find a circuit, preferably as short
as possible, that approximates a given unitary operator up to given
epsilon. For nearly two decades, the standard solution to this problem
was the SolovayKitaev algorithm, which is based on geometric
ideas. This algorithm produces circuits of size $O(\log^c(1/\epsilon))$,
where $c$ is approximately 3.97. It was a longstanding open problem
whether this exponent $c$ could be reduced to 1.
In this talk, I will report on a new class of numbertheoretic
algorithms that achieve circuit size $O(\log(1/\epsilon))$, thereby
answering the above question positively. In certain important cases,
such as the commonly used Clifford+$T$ gate set, one can even find
algorithms that are optimal in an absolute sense: the algorithm finds
the shortest circuit whatsoever for the given problem instance. This
is joint work with Neil J. Ross.
 DAVID THIBODEAU, McGill University
Programming Infinite Structures Using Copatterns [PDF]

Infinite structures are an integral part of computer science as
they serve to represent concepts such as constantly running
devices and processes or data communication streams. Due to their
importance, it is crucial for programming languages to be equipped
with adequate means to encode and reason about them.
This talk investigates the recent idea of copatterns, a device to
represent corecursive datatypes, and thus infinite structures,
dually to the usual definitions of recursive datatypes which
encode finite data. While the latter defines and analyzes data
via constructors and pattern matching, respectively, copatterns
bring to type theory a definition of corecursion using observations
and copattern matching.
 FRANK VAN BREUGEL, York University
Behavioural Distances and Simple Stochastic Games [PDF]

Behavioural pseudometrics map each pair of states of a model to
a number in the unit interval. The smaller that number, the more
alike the states behave. By identifying states that are close to
each other, we obtain a smaller model that is easier to analyze.
Several algorithms to compute behavioural pseudometrics have been
developed. In this talk, we focus on the algorithm proposed by
Bacci, Bacci, Larsen and Mardare in 2013. We show that the
algorithm can be viewed as a strategy improvement algorithm of
a simple stochastic game. As a consequence, the correctness of
the algorithm follows from the fact that strategy improvement
leads to an optimal strategy for simple stochastic games.
This is joint work with Norm Ferns and Qiyi Tang.