Connecting Effects and Uniqueness with Adoption

by John Boyland and William Retert.

Abstract

``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.

BibTeX Style Reference

@inproceedings(boyland/retert:connecting,
  author =      {John Boyland and William Retert},
  title =       {Connecting Effects and Uniqueness with Adoption},
  booktitle =   {Conference Record of POPL 2005: the 32nd
		 ACM SIGACT-SIGPLAN Symposium on Principles
		 of Programming Languages},
  month = jan,
  year = 2005,
  publisher = {ACM}}

How to Get a Copy

A Postscript preprint (or PDF) is also available here. The appendix (which is not printed in the proceedings) is available in Postscript and PDF too.


Last Modified: November 8, 2004

Connecting Effects and Uniqueness with Adoption / boyland@cs.uwm.edu