A 𝜆-Calculus for Resource Separation

Publication Information

Robert Atkey. A 𝜆-Calculus for Resource Separation. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, volume 3142 of Lecture Notes in Computer Science, 158-170. Springer, 2004.
DOI: 10.1007/978-3-540-27836-8_16

Abstract

We present a typed 𝜆-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 𝛼𝜆-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.

Additional Information

An expanded version of this work appears as part of my PhD thesis.