A lambda-calculus for resource separation

Research output: Chapter in Book/Report/Conference proceedingChapter

3 Citations (Scopus)

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

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume3142

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