An abstract category-theoretic formulation of substitution and binding

A fundamental construction in Andre Joyal's species was that of a
substitution monoidal structure on the category [P,Set], where P is
the category of natural numbers and permutations. That monoidal
structure can be used in the analysis of linear calculi to model
substitution for linear contexts, with closedness used to model
binding. That idea was investigated by Miki Tanaka, following on work
by Fiore, Plotkin and Turi, who used the category F of finite sets and
all functions in a similar way to model cartesian contexts and
cartesian binding. But this category theoretic analysis of
substitution can be done much more generally: for an arbitrary
pseudo-monad S on Cat, S1 models generalised contexts, and, given a
pseudo-distributive law of S over the (partial) pseudo-monad for free
cocompletions, there is a canonical substitution monoidal structure on
the category $[(S1)^{op},Set]$. One can give a concrete description of
the substitution monoidal structure, then an axiomatic definition of a
binding signature, extending the definitions for cartesian and linear
contexts and yielding initial algebra semantics for binding
signatures. This allows one to include structures such as those
involved with the Logic of Bunched Implications.

This is joint work with Miki Tanaka.