### 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 language | English |
---|---|

Pages (from-to) | 1091-1132 |

Number of pages | 42 |

Journal | Mathematical Structures in Computer Science |

Volume | 18 |

Issue number | 6 |

Early online date | 7 Oct 2008 |

DOIs | |

Publication status | Published - Dec 2008 |

### Keywords

- Lambda-calculus
- semantics
- logic

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

## Cite this

Collinson, M., Pym, D., & Robinson, E. (2008). Bunched Polymorphism.

*Mathematical Structures in Computer Science*,*18*(6), 1091-1132. https://doi.org/10.1017/S0960129508007159