Research

Binding signatures for generic contexts


Reference:

Power, J. and 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. Berlin: Springer, pp. 308-323. (Lecture Notes in Comput. Sci.)

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:

http://dx.doi.org/10.1007/11417170_23

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.

Details

Item Type Book Sections
CreatorsPower, J.and Tanaka, M.
DOI10.1007/11417170_23
DepartmentsFaculty of Science > Computer Science
StatusPublished
ID Code5381

Export

Actions (login required)

View Item