### Abstract

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 |

### Fingerprint

### Keywords

- Lambda-calculus
- semantics
- logic

### Cite this

*Mathematical Structures in Computer Science*,

*18*(6), 1091-1132. https://doi.org/10.1017/S0960129508007159

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

Research output: Contribution to journal › Article

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

}

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 -