TY - CHAP
T1 - Binding signatures for generic contexts
AU - Power, John
AU - Tanaka, Miki
PY - 2005
Y1 - 2005
N2 - Fiore, Plotkin and Turi provided a definition of binding signature and characterised the presheaf of terms generated from a binding signature by an initiality property. Tanaka did for linear binders what Fiore et al did for cartesian binders. They used presheaf categories to model variable binders for contexts, with leading examples given by the untyped ordinary and linear λ-calculi. Here, we give an axiomatic framework that includes their works on cartesian and linear binders, and moreover their assorted variants, notably including the combined cartesian and linear binders of the Logic of Bunched Implications. We provide a definition of binding signature in general, extending the previous ones and yielding a definition for the first time for the example of Bunched Implications, and we characterise the presheaf of terms generated from the binding signature. The characterisation requires a subtle analysis of a strength of a binding signature over a substitution monoidal structure on the presheaf category.
AB - Fiore, Plotkin and Turi provided a definition of binding signature and characterised the presheaf of terms generated from a binding signature by an initiality property. Tanaka did for linear binders what Fiore et al did for cartesian binders. They used presheaf categories to model variable binders for contexts, with leading examples given by the untyped ordinary and linear λ-calculi. Here, we give an axiomatic framework that includes their works on cartesian and linear binders, and moreover their assorted variants, notably including the combined cartesian and linear binders of the Logic of Bunched Implications. We provide a definition of binding signature in general, extending the previous ones and yielding a definition for the first time for the example of Bunched Implications, and we characterise the presheaf of terms generated from the binding signature. The characterisation requires a subtle analysis of a strength of a binding signature over a substitution monoidal structure on the presheaf category.
UR - http://dx.doi.org/10.1007/11417170_23
U2 - 10.1007/11417170_23
DO - 10.1007/11417170_23
M3 - Chapter or section
VL - 3461
T3 - Lecture Notes in Comput. Sci.
SP - 308
EP - 323
BT - Typed Lambda Calculi and Applications 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings
PB - Springer
CY - Berlin
ER -