Skip to content


Personal tools
You are here: Home » Publications » Type-checking balloon types

Type-checking balloon types

Document Actions
Up one level
Paulo Sérgio Almeida. Type-checking balloon types. MFPS XV -- mathematical foundations of program semantics, volume 20 of Electronic Notes in Theoretical Computer Science. 1999. Elsevier.

Current data abstraction mechanisms are not adequate to control sharing of state in the general case involving objects in linked structures. The pervading possibility of sharing is a source of errors and an obstacle to language implementation techniques. Balloon types, which we have introduced in~\cite{Almeida97}, are a general extension to programming languages. They make the ability to share state a first class property of a data type. The balloon invariant expresses a strong form of encapsulation: no state reachable (directly or transitively) by a balloon object is referenced by any external object. In this paper we describe the checking mechanism for balloon types. It relies on a non-trivial static analysis, described as an abstract interpretation. Here we focus in particular on the design of the abstract domain which allows the checking mechanism to work under realistic assumptions regarding possible object aliasing.

  author = "Paulo S\'ergio Almeida",
  title = "Type-checking Balloon Types",
  booktitle = "{MFPS XV} -- Mathematical Foundations of Program Semantics",
  year = "1999",
  series = "Electronic Notes in Theoretical Computer Science",
  volume = "20",
  publisher = "Elsevier",

Please read the Copyright Notice before downloading.
Created by gsd
Last modified 2004-11-24 04:30 PM
« September 2014 »
Su Mo Tu We Th Fr Sa
  1 2 3 4 5 6
7 8 9 10 11 12 13
14 15 16 17 18 19 20
21 22 23 24 25 26 27
28 29 30        

Powered by Plone

This site conforms to the following standards: