Bunched Polymorphism

Matthew Collinson, David Pym, Edmund Robinson

Research output: Contribution to journalArticle

6 Citations (Scopus)

Abstract

We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus alphalambda associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.
Original languageEnglish
Pages (from-to)1091-1132
Number of pages42
JournalMathematical Structures in Computer Science
Volume18
Issue number6
Early online date7 Oct 2008
DOIs
Publication statusPublished - Dec 2008

Fingerprint

Polymorphism
Calculus
Semantics
Multiplicative
Existential quantifier
First-order
Typed lambda Calculus
Lambda Calculus
Quantifiers
Equivalence relation
Categorical
Logic
Partial
Model

Keywords

  • Lambda-calculus
  • semantics
  • logic

Cite this

Bunched Polymorphism. / Collinson, Matthew; Pym, David; Robinson, Edmund.

In: Mathematical Structures in Computer Science, Vol. 18, No. 6, 12.2008, p. 1091-1132.

Research output: Contribution to journalArticle

Collinson, Matthew ; Pym, David ; Robinson, Edmund. / Bunched Polymorphism. In: Mathematical Structures in Computer Science. 2008 ; Vol. 18, No. 6. pp. 1091-1132.
@article{e79dbbe215034bc2ba6deb65f3b1d845,
title = "Bunched Polymorphism",
abstract = "We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus alphalambda associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.",
keywords = "Lambda-calculus, semantics, logic",
author = "Matthew Collinson and David Pym and Edmund Robinson",
year = "2008",
month = "12",
doi = "10.1017/S0960129508007159",
language = "English",
volume = "18",
pages = "1091--1132",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "6",

}

TY - JOUR

T1 - Bunched Polymorphism

AU - Collinson, Matthew

AU - Pym, David

AU - Robinson, Edmund

PY - 2008/12

Y1 - 2008/12

N2 - We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus alphalambda associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.

AB - We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus alphalambda associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.

KW - Lambda-calculus

KW - semantics

KW - logic

U2 - 10.1017/S0960129508007159

DO - 10.1017/S0960129508007159

M3 - Article

VL - 18

SP - 1091

EP - 1132

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 6

ER -