A unified category theoretic approach to variable binding

John Power

Research output: Chapter or section in a book/report/conference proceedingChapter or section

12 Citations (SciVal)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding - MERLIN '03
Place of PublicationNew York
PublisherAssociation for Computing Machinery
DOIs
Publication statusPublished - 2003

Fingerprint

Dive into the research topics of 'A unified category theoretic approach to variable binding'. Together they form a unique fingerprint.

Cite this