Speakers

Title: What is the category associated to a programming language with recursion and partiality, and can we make one from a differential language?

Abstract: This talk will introduce a famous concept in the functional programming community known as “immoral reasoning is acceptable.”  This is the first talk in a 2 talk series to develop these ideas for a functional differential programming language.   We will develop the category of partial equivalence relations for a functional programming language to give a way to move between denotations of total and partial functions.

The dual fibration, part two: partial case

Last week we reviewed how to construct the dual fibration to a given fibration, and saw that this construction gives some interesting examples.  In this second part we’ll see how to work with this idea in the setting of restriction categories.  We’ll begin by defining and working with latent fibrations (a version of the fibration notion for restriction categories), then show that certain kinds of latent fibrations have a dual.

This is joint work with Robin Cockett, Jonathan Gallagher, and Dorette Pronk.

Title: The dual fibration, part one: total case

In this talk I’ll review and discuss the dual fibration, which builds a new fibration out of an existing one by taking the opposite category of each fibre.  We’ll look at an elementary construction of this fibration due to Kock, and consider how the dual fibration plays a role in understanding reverse derivatives and lenses.

In part two, I’ll consider new work (joint with Robin Cockett, Jonathan Gallagher, and Dorette Pronk) on how to generalize these ideas to restriction categories.

Peirce’s Triadic Logic: Continuity, Modality, and L

In 1909,  in his Logic Notebook,  Charles Sanders Peirce conducted what appear to be the first experiments with many-valued logic. As these experiments are entirely contained within a handful of pages in his notebook, which were not published or discussed by other authors during his lifetime, little is known about his reasons for conducting this research.  By examining and transcribing these pages, and connecting them to his larger body of philosophy, I show how his motivations lie within his views on modality and continuity.

Title: Hyperbolic Functions for Cartesian Differential Categories

Abstract:
Hyperbolic functions are analogues of trigonemtric functions for the hyperbola. Hyperbolic functions have many applications in mathematics, physics, and engineering.

In this talk, I will generalize the hyperbolic functions sinh and cosh in Cartesian differential categories, in the same way I generalized the exponential function. In particular, the sum of these generalized hyperbolic functions will be a generalized exponential function.

A first introduction to Clifford algebras

William Kingdon Clifford (1845-78) died of tuberculosis when he was still young: he was a professor of Mathematic and Mechanics at University College, London.  His work on  “geometrical algebra” foreshadowed the theory of general relativity.  Almost a century later David Hestenes used Clifford’s ideas to develop “space-time algebra”: these ideas are still being actively developed as a basis for physics.

The talk is going to start with a very basic mathematical first introduction to “geometrical algebra”.  Applications to physics are reached by considering Clifford’s geometrical algebras in the context of tangent categories and (hopefully) I will end on some remarks in this direction.

Abadi and Plotkin’s language in terms of differential structure

Abadi and Plotkin defined the Simple Differential Programming Language (SDPL) to be a functional programming language with a first order type system where every program can be reverse differentiated.  Importantly this language has conditionals and recursive functions.  In this talk we will develop the denotational semantics and source code transformation semantics from a categorical point of view using the technology of reverse differential join restriction categories.  In particular, using an interpretation into such a category we will show that source code transformations are modelled correctly, that the trace-differentiation technique is modelled, and we will express a denotational semantics for SDPL into any such category with enough points.   Finally, we will use the theory of these categories to derive a modification to the operational semantics that yields an exponential speedup on the differentiation of loops.  Also, as a bonus, we will do recursion in a restriction category!

Rho calculus

Process calculus is a family of related approaches to formally model concurrent systems, e.g. Pi-calculus which pass channels as data along other channels; Ambient calculus which models distributed and mobile computations. Rho Calculus (Reflective Higher Order Calculus) is based on Pi-calculus; it is a closed theory in the form of an asynchronous message-passing calculus built on a notion of quoting. Names are quoted processes and unquoting is reification of processes. Names are subject to algebraic rules and reasoning such as substitutions and bisimulation.

Title: Microlinear Lawvere theories

Abstract:
In this talk we introduce Microlinear Lawvere theories, and show that differential objects in cartesian tangent categories are an example. One of the more striking applications of this theory is that every tangent category embeds into the Eilenberg-Moore category of a tensor differential category.

(Joint work with Jonathan Gallagher and Rory Lucyshyn-Wright)

Title: The symmetric algebra’s other universal properties (joint work with Richard Garner)

Abstract:
The symmetric algebra is known for being the free commutative algebra over a vector space. Therefore, it is universal amongst commutative algebras. It turns out, the symmetric algebra also has another universal property which can be used to construct the initial monoidal differential modality.