We give a general category theoretic formulation of the approach to modelling variable binding first proposed by Fiore, Plotkin, and Turi. This general formulation allows us to include variable binding as they have it, as well as Tanaka's linear variable binding and variable binding for other binders and for mixtures of binders as for instance in the Logic of Bunched Implications. The key structure developed by Fiore et al. was a substitution monoidal structure, from which their formulation of binding was derived; so we give an abstract formulation of a substitution monoidal structure, then, at that level of generality, derive the various category theoretic structures they considered. The central construction we use is that of a pseudo-distributive law between 2-monads on Cat, which suffices to induce a pseudo-monad on Cat, and hence a substitution monoidal structure on the free object on 1.
|Title of host publication||Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding - MERLIN '03|
|Place of Publication||New York|
|Publisher||Association for Computing Machinery|
|Publication status||Published - 2003|