A unified category-theoretic formulation of typed binding signatures

Miki Tanaka, John Power

Research output: Chapter in Book/Report/Conference proceedingChapter

10 Citations (Scopus)

Abstract

We generalise Fiore et al's account of variable binding for untyped cartesian contexts and Tanaka's account of variable binding for untyped linear contexts to give an account of variable binding for simply typed axiomatically defined contexts. In line with earlier work by us, we axiomatise the notion of context by means of a pseudo-monad S on Cat: Fiore et al implicitly used the pseudo-monad Tfp for small categories with finite products, and Tanaka implicitly used the pseudo-monad Tsm for small symmetric monoidal categories. But here we also extend from untyped variable binding to typed variable binding. Given a set A of types, this involves generalising from Fiore et al's use of [F,Set] to [(SA)op,SetA]. We define a substitution monoidal structure on [(SA)op,SetA], give a definition of binding signature at this level of generality, and extend initial algebra semantics to this typed, axiomatic setting. This generalises and axiomatises previous work by Fiore et al and later authors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, and it yields an improved axiomatic definition of binding signature even in the case of untyped binders.
Original languageEnglish
Title of host publicationMERLIN '05 Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding
Place of PublicationNew York
PublisherAssociation for Computing Machinery
Pages13-24
Number of pages12
ISBN (Print)1-59593-072-8
DOIs
Publication statusPublished - 2005

Fingerprint Dive into the research topics of 'A unified category-theoretic formulation of typed binding signatures'. Together they form a unique fingerprint.

Cite this