A unified category theoretic approach to variable binding


Power, J., 2003. A unified category theoretic approach to variable binding. In: Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding - MERLIN '03. New York: ACM.

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:


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.


Item Type Book Sections
CreatorsPower, J.
DepartmentsFaculty of Science > Computer Science
ID Code26503


Actions (login required)

View Item