### Abstract

We present a typed lambda-calculus for recording resource separation constraints between terms. The calculus contains a novel way of manipulating nested multi-place contexts augmented with constraints, allowing a concise presentation of the typing rules. It is an extension of the affine alpha-lambda-calculus. We give a semantics based on sets indexed by resources, and show how the calculus may be extended to handle non-symmetric relations with application to allowable information flow. Finally, we mention some future directions and questions we have about the calculus.

Original language | English |
---|---|

Title of host publication | Automata, Languages and Programming: 31st International Colloquium, ICALP 2004 |

Publisher | Springer |

Pages | 158-170 |

Number of pages | 13 |

ISBN (Print) | 9783540228493 |

DOIs | |

Publication status | Published - 2004 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 3142 |

### Keywords

- function type
- natural transformations
- transitive closure
- linear logic
- structural rule

## Fingerprint Dive into the research topics of 'A lambda-calculus for resource separation'. Together they form a unique fingerprint.

## Cite this

Atkey, B. (2004). A lambda-calculus for resource separation. In

*Automata, Languages and Programming: 31st International Colloquium, ICALP 2004*(pp. 158-170). (Lecture Notes in Computer Science; Vol. 3142). Springer. https://doi.org/10.1007/978-3-540-27836-8_16