Affiliations: School of Informatics, University of Edinburgh, King's
Buildings, Edinburgh EH9 3JZ, Scotland. E-mail: ajp@inf.ed.ac.uk | National Institute of Information and Communications
Technology, 4-2-1 Nukui-Kitamachi, Koganei, Tokyo 184-8795, Japan. E-mail:
miki.tanaka@nict.go.jp
Note: [] Address for correspondence: School of Informatics, University of
Edinburgh, King's Buildings, Edinburgh EH9 3JZ, Scotland
Abstract: We generalise Fiore et al's account of variable binding for untyped
cartesian contexts to give an account of binding for either variables or names
that may be typed. We do this in an enriched setting, allowing the
incorporation of recursion into the analysis. Extending earlier work by us, we
axiomatise the notion of context by defining and using the notion of an
enriched pseudo-monad S on V-Cat, with leading examples of V given by Set and
ωCpo, the latter yielding an account of recursion. Fiore et al implicitly
used the pseudo-monad T_{fp} on Cat for small categories
with finite products. Given a set A of types, our extension to typed binders
and enrichment involves generalising from Fiore et al's use of [F, Set] to
[(SA)^{op}, V^{A}]. We define a
substitution monoidal structure on [(SA)^{op},
V^{A}], allowing us to give a definition of binding
signature at this level of generality, and extend initial algebra semantics to
the typed, enriched axiomatic setting. This generalises and axiomatises
previouswork by Fiore et al and later authors in particular cases. In
particular, it includes the Logic of Bunched Implications and variants,
infinitary examples, and structures not previously considered such as those
generated by finite limits.
