Personal tools
You are here: Home Events Abstract Archives 2005 Binding Signature for Generic Contexts

Binding Signature for Generic Contexts

Miki Tanaka National Institute of Information and Communications Technology Japan 4pm, Thursday 27 January 2005 Room 2511, JCMB, King's Buildings

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 \lambda-calculi.

In this talk, I give an axiomatic framework that includes Fiore et al's work on cartesian and Tanaka's work on linear binders, and moreover their assorted variants, 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.

Document Actions