Bunched Polymorphism

Matthew Collinson, David Pym, Edmund Robinson

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)


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
Issue number6
Early online date7 Oct 2008
Publication statusPublished - Dec 2008


  • Lambda-calculus
  • semantics
  • logic


Dive into the research topics of 'Bunched Polymorphism'. Together they form a unique fingerprint.

Cite this