TY - CHAP

T1 - On bunched polyrnorphism

AU - Collinson, M

AU - Pym, D

AU - Robinson, E

N1 - ID number: ISI:000232244900005

PY - 2005

Y1 - 2005

N2 - We describe a polymorphic extension of the substructural lambda calculus alpha lambda associated with the logic of bunched implications. This extension is particularly novel in that both variables and type variables are treated substructurally, being maintained through a system of zoned, bunched contexts. Polymorphic universal quantifiers are introduced in both additive and multiplicative forms, and then metatheoretic properties, including subject-reduction and normalization, are established. A sound interpretation in a class of indexed category models is defined and the construction of a generic model is outlined, yielding completeness. A concrete realization of the categorical models is given using pairs of partial equivalence relations on the natural numbers. Polymorphic existential quantifiers axe presented, together with some metatheory. Finally, potential applications to closures and memory-management are discussed.

AB - We describe a polymorphic extension of the substructural lambda calculus alpha lambda associated with the logic of bunched implications. This extension is particularly novel in that both variables and type variables are treated substructurally, being maintained through a system of zoned, bunched contexts. Polymorphic universal quantifiers are introduced in both additive and multiplicative forms, and then metatheoretic properties, including subject-reduction and normalization, are established. A sound interpretation in a class of indexed category models is defined and the construction of a generic model is outlined, yielding completeness. A concrete realization of the categorical models is given using pairs of partial equivalence relations on the natural numbers. Polymorphic existential quantifiers axe presented, together with some metatheory. Finally, potential applications to closures and memory-management are discussed.

M3 - Chapter or section

SN - 0302-9743

VL - 3634

T3 - Lecture Notes in Computer Science

SP - 36

EP - 50

BT - Computer Science Logic, Proceedings

ER -