Personal tools
You are here: Home Fluid Publications POPL Permissions Abstract
Document Actions

POPL Permissions Abstract

by John Boyland last modified 2005-03-07 03:31 PM

Abstract of POPL paper: Connecting Effects and Uniqueness with Adoption

``Adoption'' is when one piece of state is logically embedded in another piece of state. Adoption provides information hiding (the adopter can be used as a proxy for the adoptee) and with linear existentials, provides a way to store unique pointers in shared state. In this paper, we give an operational semantics of adoption in a simple procedural language with pointers to records. We define a ``permission'' type-system that uses adoption to model both effects and uniqueness. We prove type soundness (well-typed programs don't go wrong) and state separation (separately-typed statements cannot access the same state). Then we show how high-level effects and uniqueness annotations can be expressed in the type-system. The distinction between read and write effects is ignored in the body of this paper.

 

Powered by Plone, the Open Source Content Management System

This site conforms to the following standards: