A Unified Category-Theoretic Formulation of Typed Binding Signatures

MERLIN 2005

数学;计算机科学

Miki Tanaka ; John Power

Others  :  http://homepages.inf.ed.ac.uk/rpollack/TYPES/MERLIN_05/p13-tanaka.pdf
PID  :  52667

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

We generalise Fiore et al’s account of variable binding for untyped cartesian contexts and Tanaka’s account of vari- able 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 [, Set] to [(SA)op, SetA]. We define a substitution monoidal struc- ture on [(SA)op, SetA], give a definition of binding signa- ture 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 au- thors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, and it yields an im- proved axiomatic definition of binding signature even in the case of untyped binders. Categories and Subject Descriptors D.3.1 [Programming Lan- guages]: Formal Definitions and Theory; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Lan- guages General Terms Theory ∗This work has been done with the support of EPSRC grant GR/586372/01: A Theory of Effects for Programming Lan- guages. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. MERLIN’05 September 30, 2005, Tallinn, Estonia. Copyright 2005 ACM 1-59593-072-8/05/0009 ...$5.00.