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.
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|
|Departments||Faculty of Science > Computer Science|
Actions (login required)