A lambda-calculus for resource separation

Research output: Chapter in Book/Report/Conference proceedingChapter

4 Citations (Scopus)
44 Downloads (Pure)


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 languageEnglish
Title of host publicationAutomata, Languages and Programming: 31st International Colloquium, ICALP 2004
Number of pages13
ISBN (Print)9783540228493
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science


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


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

Cite this