UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Bunching for Regions and Locations

Collinson, M; Pym, D; (2006) Bunching for Regions and Locations. Electronic Notes in Theoretical Computer Science , 158 (1) pp. 171-197. 10.1016/j.entcs.2006.04.010.

Full text not available from this repository.

Abstract

There are a number of applied lambda-calculi in which terms and types are annotated with parameters denoting either locations or locations in machine memory. Such calculi have been designed with safe memory-management operations in mind. It is difficult to construct directly denotational models for existing calculi of this kind. We approach the problem differently, by starting from a class of mathematical models that describe some of the essential semantic properties intended in these calculi. In particular, disjointness conditions between regions (or locations) are implicit in many of the memory-management operations. Bunched polymorphism provides natural type-theoretic mechanisms for capturing the disjointness conditions in such models. We illustrate this by adding regions to the basic disjointness model of αλ, the lambda-calculus associated to the logic of bunched implications. We show how both additive and multiplicative polymorphic quantifiers arise naturally in our models. A locations model is a special case. In order to relate this enterprise back to previous work on memory-management, we provide an example in which the model is refined and used to provide a denotational semantics for a language with explicit allocation and disposal of regions. © 2006 Elsevier B.V. All rights reserved.

Type: Article
Title: Bunching for Regions and Locations
DOI: 10.1016/j.entcs.2006.04.010
UCL classification: UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: http://discovery.ucl.ac.uk/id/eprint/1495330
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item