Last Update: 2019-05-22. For updates or additions to this page, please send a note to Robin Cockett.

Attendees, Abstracts, and Slides

Title: Tangent categories tutorial I: Multivariable calculus
Abstract: These tutorials will introduce the subject of tangent categories via two very different approaches.  In the first part, we'll focus on what the tangent category axioms looks like in the "category of multivariable calculus": the category whose objects are open subsets of R^n's and whose maps are smooth functions between them. In this tangent category, the axioms can be seen as representing familiar properties of the derivative (such as the symmetry of mixed partial derivatives).  We'll also look at how understanding what properties these axioms represent can be helpful in formulating and proving differential geometric ideas in an arbitrary tangent category.

Title: Abstract Datatypes in Differential programming
Abstract: In this talk we will discuss some first steps in formalizing abstract data types for differential (total, functional) programming. Following the classical setting where the semantics for a functional programming language is given by some cartesian closed category Sem, we take Barr and Wells’ perspective that an Abstract Data Type is a Sketch.
For a functional differential programming language, we will use Cockett and Gallagher’s work and take a coherently closed tangent category as our semantics category. This introduces the problem: what are abstract data types in this setting? Following Garner and Leung’s work, we may regard tangent categories as certain sorts of enriched categories. We may then build off of Barr and Wells’ work using Kelly’s notion of enriched sketches, and present some examples.

Title: The presheaf of scalar functions and the internal rig of scalars of a cartesian tangent category
Abstract: Tangent categories allow various aspects of differential geometry to be developed in an abstract setting without any mention of a ring of scalars.  Nevertheless, we shall show that every cartesian tangent category has an associated notion of scalar-valued function.  Indeed, we shall show that every cartesian tangent category has an associated presheaf of commutative rigs (i.e., rings without negatives), which we call the presheaf of scalar functions.  In the classical case of smooth manifolds, this presheaf is isomorphic to the presheaf that associates to each smooth manifold its ring of smooth, real-valued functions.  In any cartesian tangent category, we can ask whether the presheaf of scalar functions is representable, in which case the representing object R is an internal commutative rig, which we call the rig of scalars.  In this case, every tangent bundle carries the structure of an internal fibrewise R-module.  For an arbitrary cartesian tangent category, the presheaf of scalar functions sends each object M to a rig that consists of certain linear endomorphisms of the tangent functor on the simple slice over M.  Consequently, the presheaf of scalar functions and the internal rig of scalars can be seen as fibred, enriched, or internal analogues of Rosick\'y's ring of endomorphisms of an abstract tangent functor.  The definition of the internal rig of scalars in the above sense is a priori distinct from the other approaches to scalars in tangent categories that have been proposed, including recent work of Gallagher, MacAdam, and the speaker (on representable units) and earlier work of Cockett and Cruttwell on line objects in representable tangent categories, drawing on ideas of Lawvere and Rosick\'y; the relation of the internal rig of scalars to these other formulations remains to be investigated.

Title: Multicategories of multiary lenses
Abstract: Recently Diskin and Konig proposed a definition of multidirectional transformation generalizing the bidirectional case to allow multiple data sources. They give both  a ``propagation'' form (in the style of the symmetric delta lenses of Diskin et al), and a ``wide span'' form (in the style of the authors). In common with classical symmetric lenses, the ``multiary lenses''  should be studied modulo equivalence relations that factor out differences in hidden data from the observable behaviour. Modulo the equivalence relations the relationship between the two styles needs to be established. This will be explained. More significantly, the first proposed compositions of multiary lenses have limitations: so-called "well-behaved amendment lenses" don't necessarily compose; some kinds of compositions might not always be defined; and in any case, composition of multiary lenses cannot be expected to form a category - since there are more than two data sources there are not even well-defined notions of domain or codomain. We introduce a class of asymmetric amendment lenses called spg-lenses (stable put-get lenses) that is more general than well-behaved amendment lenses, but is closed under composition, and show how to use spg-lenses to define, via wide spans, a class of mutidirectional transformations which compose well and form a multicategory. (This is joint work with Michael Johnson).

Title: Synthetic $\infty$-category theory and $\infty$-cosmology
Abstract: Applications of homotopy theory are ubiquitous in many fields of mathematics; celebrated examples include those that abound in algebraic geometry and algebraic K-theory. While these are all recognisably homotopical in essence, relatively few find natural expression in the traditional category of topological spaces and continuous maps. Instead, we work within an abstractly defined homotopy theory of generalised spaces specifically adapted to the application at hand. Examples of homotopy theories of this kind include those that apply to various varieties of spectra, simplicial sheaves and schemes, mixed motives, operads, and so forth. In recent times we have come to use the term $\infty$-category to refer to any structure designed to axiomatise (aspects of) these abstract homotopy theories. Indeed we might say, rather presumptuously, that $\infty$-categories provide the context for synthetic accounts of homotopy theory. 
The past two decades have seen the development of a veritable panoply of $\infty$-categorical notions. Where once the model categories of Quillen and the triangulated categories of Verdier sufficed for most purposes, many more recent applications have populated the homotopical zoo with a great variety of exotic $\infty$-categorical species. Notable beasts of this kind include simplicial categories, quasi-categories, (complete) Segal spaces and categories, relative categories, Theta-sets, complicial sets, and many variants on these themes. Some of these come equipped with a fully developed homotopical category theory, but most enjoy only a folkloric account of the basic categorical tropes such as limits, colimits, Kan extensions, monads and monadicity, generator properties, Grothendieck fibrations and so forth.
In this workshop series we propose to survey the $\infty$-categorical zoo from the air. In doing so we shall develop a map describing how the category theory of $\infty$-categories may be developed in a way that is largely model independent. By analogy with traditional accounts of categorical foundations, wherein we study categories of various kinds by interrogating abstract properties of the 2-categories in which they live, the essence of our approach will be the axiomatic study of $\infty$-category theory within certain $(\infty,2)$-categories. More specifically, we shall make our $(\infty,2)$-categories concrete by studying $\infty$-cosmoi, these being certain simplicially enriched categories of fibrant objects. We shall see how $\infty$-categorical theories, of limits and colimits, Grothendieck fibrations, (point-wise) Kan extension, monads and Beck monadicity and so forth, may be developed in this context.
As a form of ur-witticism, we shall adopt the term $\infty$-cosmology for the form of synthetic $\infty$-category theory presented in this course. This work is joint with Emily Riehl and is the subject of a book in development entitled ``Elements of $\infty$-Category Theory'', the current draft of which may be found here.

Title: Complete positivity for mixed unitary categories
Abstract:  In this talk we generalize the $\CP^\infty$-construction of dagger monoidal categories to mixed unitary categories.  Mixed unitary categories provide a setting, which generalizes (compact) dagger monoidal categories and in which one may study quantum processes of arbitrary dimensions.
We show that the existing results for the $\CP^\infty$-construction hold in this more general setting. In particular, we generalize the notion of environment structures to mixed unitary categories and show that the  $\CP^\infty$-construction on mixed unitary categories is characterized by this generalized environment structure.

Title: Weakening of the Conditions for a Bicategory of Fractions
Abstract: In this talk I will address two issues that make bicategories of fractions hard to work with: the size of the hom-categories and the equivalence relation on the 2-cells. I will discuss conditions on a class of arrows to be inverted in a bicategory, which is not closed under composition, to still give a bicalculus of fractions. This is a useful result when one tries to reduce the class of arrows to be inverted in order to to obtain small hom-categories in the bicategory of fractions.
I will also discuss conditions under which there are canonical representatives for the equivalence classes of 2-cells that simplify the rules for horizontal pasting.
I will briefly mention examples of bicategories and classes of arrows to which these results apply.  This is joint work with Laura Scull.

Title:  Continuous monads:  continuous lattices revisited.
Outline:
(1)  Lattices for computation.
(2)  Motivating monads.
(3)  Conditionals.
(4)  Power set monads.
(5)  Continuous monads
(6) The two-element algebra
(7) Scott monads.

Title:  One-and-a-Half Simple Differential Programming Languages
Abstract: Languages for learning pose interesting foundational challenges. We look at one case: the foundations of differentiable programming languages with a first-class differentiation operator. Graphical and linguistic facilities for differentiation have proved their worth over recent years for deep learning (deep learning makes use of gradient descent optimisation methods to choose weights in neural nets). Automatic differentiation, also known as algorithmic differentiation, goes much further back, at least to the early 1960s, and provides efficient techniques for differentiation, e.g., via source code transformation. It seems fair to say, however, that differentiable programming languages have begun to appear only recently. It seems further fair to say that, while there has certainly been some foundational study of differentiable programming languages, there is ample opportunity to do more.
We investigate the semantics of a simple first-order functional programming language with reals, product types, and a first-class reverse-mode differentiation operator (reverse-mode differentiation generalises gradients). The semantics employs a standard concept of real analysis: smooth multivariate functions with open domain. It turns out that such partial functions fit well with programming constructs such as conditionals and recursion; indeed they form a complete partial order, and so standard fixed-point methods can be applied.  We  give an operational semantics which, roughly, can be seen as a formalisation of a version of the trace (or tape) method used to implement automatic differentiation. The semantics consists of three parts: ordinary evaluation, symbolic evaluation to eliminate control constructs, and a source-code transformation to symbolically differentiate terms with no control constructs,
From a programming language point of view, however, many types are lacking, particularly sum types and recursive types, such as lists. We conclude with a brief presentation of notions of shapely datatypes and smooth functions. These can be used to give the semantics of such types and the usual functions between them while retaining first-class differentiation.
This work constitutes only an initial exploration, and we look forward to a rich field connecting two worlds: programming languages and their foundations, and real analysis and allied areas of mathematics.

Title: Tangent categories tutorial II: Weil algebras and tangent categories.
Abstract: These tutorials will introduce the subject of tangent categories via two very different approaches. In the second part, we'll focus on how the tangent category axioms
arise from Weil algebras.  We will introduce Weil algebras, along with their tangent functor, and we will see a sense in which this tangent structure determines all
tangent structures (Leung's theorem).  This will allow us to view tangent categories as enriched categories (Garner's theorem), and we will look at a few applications  to the theory of tangent categories form this point of view.

Title: Differential programming languages via tangent categories
Abstract: This talk (for a rainy afternoon!) will introduce an ongoing project to formalize differential programming languages using restriction tangent categories.  We will introduce a simple forward mode differential programming language, and give a semantics for this language into a differential join restriction category.  We will begin the exploration of coinductive datatypes by describing comonads whose coKleisli categories are tangent categories (hence coKleisli computations can be 'differentiated').  We will then show how to extend this with total function spaces, and we will highlight a subtlety that arises when trying to extend with internal homs for partial functions. 

Title:  An introduction tutorial on tensor (co)differential categories and Cartesian differential categories
Abstract: Part one of this tutorial will introduce (tensor) differential categories and the dual notion of codifferential categories. Differential categories provide the categorial semantics of differential linear logic, while the structure of a codifferential category axiomatizes the basic algebraic foundations of differential calculus. Part two of this tutorial will introduce Cartesian differential categories, whose axioms generalize the directional derivative from multivariable calculus and (with an extra axiom) provide the categorial semantics of the differential $\lambda$-calculus. In particular, the coKleisli category of a differential category is a Cartesian differential category.

Title: Circuit relations for real stabilizers: towards TOF + H!
Abstract: The real stabilizer fragment of quantum mechanics was shown to have a complete axiomatization in terms of the angle-free fragment of the ZX-calculus. This fragment of the ZXcalculus--although abstractly elegant--is stated in terms of identities, such as spider fusion which generally do not have interpretations as circuit transformations. We complete the category CNOT generated by the controlled not gate and the computational ancillary bits, presented by circuit relations, to the real stabilizer fragment of quantum mechanics. This is performed first, by adding the Hadamard gate and the scalar sqrt 2 as generators. We then construct translations to and from the angle-free fragment of the ZX-calculus, showing that they are inverses. We remove the generator sqrt 2 and then prove that the axioms are still complete for the remaining generators. This yields a category which is not compact closed, where the yanking identities hold up to a non-invertible, non-zero scalar. We then discuss how this could potentially lead to a complete axiomatization, in terms of circuit relations, for the approximately universal fragment of quantum mechanics generated by the Toffoli gate, Hadamard gate and computational ancillary bits.

Title: Tangent ∞ -categories and Goodwillie calculus
Abstract: In these talks, I will describe joint work (in progress) with Kristine Bauer and Matthew Burke on tangent structures in higher category theory. Using Leung's work on Weil algebras, we introduce a definition of tangent structure on an ∞-category (or, more generally, on any object in an (∞,2)-category). I will highlight the ways in which the usual tangent category axioms are weakened in the ∞-categorical setting. As a modest start to the theory of tangent ∞-categories, I will propose a definition for differential objects in this setting.
The main goal of this work is to capture the following example: a tangent structure on the ∞-category of (presentable) ∞-categories. In this case, a "tangent bundle functor" for presentable ∞-categories has already been defined by Lurie in the context of deformation theory. Our project amounts to verifying that Lurie's construction of the tangent bundle functor extends to a full tangent structure. The key steps in this argument are based on Goodwillie's calculus of functors, and our long-term goal is to relate Goodwillie's ideas more explicitly to the theory of tangent (∞-)categories.

Title: Tracelets and Tracelet Analysis Of Compositional Rewriting Systems
Abstract: Taking advantage of a recently discovered associativity property of rule compositions, we extend the classical concurrency theory for rewriting systems over adhesive categories. We introduce the notion of tracelets, which are defined as minimal derivation traces that universally encode sequential compositions of rewriting rules. Tracelets are compositional, capture the causality of equivalence classes of traditional derivation traces, and intrinsically suggest a clean mathematical framework for the denition of various notions of abstractions of traces. We illustrate these features by introducing a rst prototype for a framework of tracelet analysis, which as a key application permits to formulate a rst-of-its-kind algorithm for the static generation of minimal derivation traces with prescribed terminal events.

Title: Introduction to etale groupoids and constructing convolution algebras for them via finiteness spaces
Abstract: We'll go through the basic examples and definitions associated to etale groupoids. We'll then show how to construct convolution algebras associated to them using the results of "Finiteness spaces and generalized power series" by Blute, Cockett, Jacqmin and Scott.  It depends crucially on work of Beauvais-Feisthauer, Dewan and Drummond, who show how topological spaces can be viewed as finiteness spaces.

Title: A representation for inverse semigroups
Abstract: It is well-known that every inverse semigroup fits into a short exact sequence induced by the largest idempotent-separating congruence on the semigroup. However, this does not mean that we can always present a semigroup using the corresponding semidirect product. In this talk I will show using topos-theoretic methods that a slightly more general semidirect product, namely with a connected groupoid, suffices to recover every inverse semigroup up to Morita equivalence.
This is joint work with Jonathan Funk.

Title: Computable Functions in Categories
Abstract: I will survey some results on computable functions in categories, in particular in free (syntactic) ones. This is part of a survey on this subject being written with Pieter Hofstra. In addition to older work on free cartesian, symmetric monoidal, and cartesian closed categories, I hope to report about work in progress with Yan Steimle on provably total and partial recursive functions in Heyting and Peano arithmetic, and discuss the question:  does the classifying category of Heyting Arithmetic form a Turing category (or a lax version thereof)?  This seems to require new versions of Church's Rule, and other syntactic machinery not previously discussed in the literature.

Title: Derivatives of encoded Turing machines in linear logic
Abstract: I will discuss joint work with James Clift which examines concretely the derivatives in the sense of Ehrhard-Regnier of (a modified form of) Girard’s encoding of Turing machines into linear logic. These are rather simple proofs, but computing with the denotations of their derivatives in the vector space semantics reveals a natural connection between Ehrhard-Regnier derivatives and the propagation of a naive form of probability through linear logic proofs. This naive probability is closely related to continuous relaxations of computational graphs that have been explored in an ad-hoc way by various groups in connection with program synthesis and machine learning.

Title: A Site for Geometrizing Quasicharacters
Abstract: In this talk we will show how to produce a topology on the category of formal schemes over an integral p-adic ring that allows us to geometrize quasicharacters of p-adic schemes. In particular, we will describe what quasicharacters are, how they arise in the p-adic Local Langlands Programme, and how to use category theory to show, in many cases, that they can be viewed as functions defined on a scheme.

Title: Involution algebroids: a generalisation of Lie algebroids for tangent categories
Abstract: We define involution algebroids which generalise Lie algebroids to the abstract setting of tangent categories. As a part of this generalisation the Jacobi identity which appears in classical Lie theory is replaced by an identity similar to the Yang-Baxter equation. We sketch how every groupoid in a tangent category is approximated by an involution algebroid. In addition we describe the appropriate definitions of admissible paths and admissible homotopies in an involution algebroid and use a curve object to transport vectors along them. This is joint work with Ben MacAdam.

Title: Categorical constructions in graphs
Abstract: I will present some categorical constructions in the category of graphs.  This will be an extremely elementary talk discussing the way I have been using graphs to introduce my undergraduate students to categorical concepts, and the work they have been doing with them.

Title: A Generalization of The Invariant Topological Complexity
Abstract: The invariant topological complexity was introduced by Lubawski and Marzantowicz in order to estimate the complexity of $G$-spaces. This invariant is related to the motion planning algorithm of a robot, specially when the robot or its configuration space is symmetric.
In this talk, I will introduce the higher invariant topological complexity which is a generalization of the invariant topological complexity and I will discuss some properties of this new invariant.

Title: On Matrix Factorizations
Abstract: We introduce the notion of matrix factorizations, an algebraic construction of great utility in commutative algebra and quantum physics among many other applications. Yoshino defined the tensor product of matrix factorizations denoted ⊗ which is such that if X and Y are respectively matrix factorizations of power series f and g, then X⊗Y is a matrix factorization of the sum f + g. We introduce a new bifunctorial operation denoted ⊗ which is such that X ⊗Y is a matrix factorization of the product of the power series f g. We also prove some properties of ⊗ .

Time permitting, we give an application of matrix factorizations by recalling the construction of the bicategory LG_K of Landau-Ginzburg models whose objects are polynomials and 1-morphisms are matrix factorizations.

Title: Spatially Induced Concurrency within Presheaves of Labelled Transition Systems
Abstract: The theory of concurrency developed through a variety of models such as Petri nets, event structures and labelled transition systems with independence. Yet most of these models describe concurrency as an abstract relation on transitions (or events) of a system whose axioms enforce patterns of behavior for concurrent transitions, without giving a basis as to why concurrency might arise in such systems in the first place. For this talk, we will present a very natural form of induced concurrency that arises in a spatially distributed system modelled as a presheaf from a complete Heyting algebra (whose elements are regions of space, under inclusion) to the category of labelled transitions systems. With minimal axioms imposed on such presheaves, we get a Theorem of Spatially Induced Independence that yields various patterns of commutativity for transitions that don't interfere with each other's regions of dependencies and effects in space. The current aim is to extend these results to process models where transitions can be characterized as continuous or smooth maps from a path shape to a topological space or a manifold over the set of states. More specifically, we are investigating whether the theory of concurrency and spatially induced independence can be carried over to the context of physics, to be treated uniformly along with concurrency in computer science.

Title: Split Opfibrations and Cofunctors
Abstract: Split opfibrations, also known in computer science as c-lenses, may be characterised as algebras for a particular KZ-monad, and are important in the study of least-change synchronisation between systems such as databases. In this talk, I will use cofunctors to introduce two alternative ways of defining split opfibrations between small categories: the first utilising double categories and the second utilising the décalage of a category. I will explore how these definitions are linked, and discuss consequences for the study of lenses using internal category theory.

Title: Complex numbers in a topos
Abstract: TBA

Title:  A short survey on Chu
Abstract: A short survey on Chu in three parts.
(1)  Early core material in my 1999 Coimbra notes (20 minutes)
(2)  The sense in which 1 and  ⊥ jointly generate/cogenerate Chu(Set, Chu(1, ⊥)). (5 minutes)
(3)  Generalization of Chu(1, ⊥) to the bimodule  ℒ ⇏J. (15 minutes)

Title: Global warming and determining feedback contributions
Abstract: Now for something completely different!  (For a rainy afternoon!)
Decadal, centennial, and millennial climate feedbacks are of increasing strength. This follows from the relevant theory, as well as from the 35+ CMIP5 models which all agree that TCR < ECS < ESS.
However neither theory nor models are in agreement on the strengths of those feedbacks, raising the question of whether there is a more transparent way of determining them than has proved thus far to be possible with models.
One way to measure the overall contribution of all feedbacks would be to shine an accurately calibrated radiator at Earth and observe how the surface warms in response to an increase in radiative flux. If it behaves according to Stefan-Boltzmann, flux SB(T) = σT^4, it is reasonable to infer that the Planck feedback is the only one. Any departure from SB could then reasonably be taken as an indication of the presence of other feedbacks.
In this work we exploit a previously unexploited feature of centennial climate, namely that the considerable chatter in HadCRUT4 at shorter time scales essentially disappears at centennial scales with the exception of just two components, CO2 and total solar irradiance or TSI. This is evidenced by the residual when HadCRUT4 is modeled as 1.87*RF + 0.32*TSI (blue curve in Fig. 1) where RF = log2(CO2). Whereas the standard of this residual is 146 mK, smoothing it to a running mean of 11 years to remove the solar cycle and then 65 years to remove the Atlantic Multidecadal Oscillation (red curve in Fig. 1) reduces its standard deviation to a mere 2.8 mK, thereby demonstrating the essential absence of any components of centennial climate besides the two in the model.
Figure 2  shows the smoothed versions of our data. Figure 3 compares HadCRUT4 detrended by 1.87*RF with 0.32*TSI, showing that RF and TSI are the only significant components of centennial HadCRUT4.We can now restate this centennial climate model as (1.02*RF + 0.175*TSI)/(3.74*(1 - g)) where (i) 0.175 = (1 - A)/4 where A = 0.3 is the albedo and 4 is surface/cross-section for a sphere; (ii) gain g = 0.854 inferred from (i); (iii) the Charney constant 3.74 watts/m2/K is the value of the derivative of the Stefan-Boltzmann law at Earth's effective temperature; and (iv) 1.02 is the no-feedback sensitivity of centennial climate CO2 inferred from the feedback value 1.87 and the denominator.

Back to the main page for Foundational Methods in Computer Science 2019.