Binding signatures for generic contexts

John Power, Miki Tanaka

Research output: Chapter in Book/Report/Conference proceedingChapter

5 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings
Place of PublicationBerlin
PublisherSpringer
Pages308-323
Number of pages16
Volume3461
DOIs
Publication statusPublished - 2005

Publication series

NameLecture Notes in Comput. Sci.
PublisherSpringer

Fingerprint

Presheaves
Signature
Cartesian
Lambda Calculus
Term
Substitution
Context
Logic

Cite this

Power, J., & Tanaka, M. (2005). Binding signatures for generic contexts. In Typed Lambda Calculi and Applications 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings (Vol. 3461, pp. 308-323). (Lecture Notes in Comput. Sci.). Berlin: Springer. https://doi.org/10.1007/11417170_23

Binding signatures for generic contexts. / Power, John; Tanaka, Miki.

Typed Lambda Calculi and Applications 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings. Vol. 3461 Berlin : Springer, 2005. p. 308-323 (Lecture Notes in Comput. Sci.).

Research output: Chapter in Book/Report/Conference proceedingChapter

Power, J & Tanaka, M 2005, Binding signatures for generic contexts. in Typed Lambda Calculi and Applications 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings. vol. 3461, Lecture Notes in Comput. Sci., Springer, Berlin, pp. 308-323. https://doi.org/10.1007/11417170_23
Power J, Tanaka M. Binding signatures for generic contexts. In Typed Lambda Calculi and Applications 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings. Vol. 3461. Berlin: Springer. 2005. p. 308-323. (Lecture Notes in Comput. Sci.). https://doi.org/10.1007/11417170_23
Power, John ; Tanaka, Miki. / Binding signatures for generic contexts. Typed Lambda Calculi and Applications 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings. Vol. 3461 Berlin : Springer, 2005. pp. 308-323 (Lecture Notes in Comput. Sci.).
@inbook{8ceb7157d6bc4821ba99f8ad4328aef0,
title = "Binding signatures for generic contexts",
abstract = "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.",
author = "John Power and Miki Tanaka",
year = "2005",
doi = "10.1007/11417170_23",
language = "English",
volume = "3461",
series = "Lecture Notes in Comput. Sci.",
publisher = "Springer",
pages = "308--323",
booktitle = "Typed Lambda Calculi and Applications 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings",

}

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

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 -