A step-indexed model of substructural state

The concept of a "unique" object arises in many emerging programming languages such as Clean, CQual, Cyclone, TAL, and Vault. In each of these systems, unique objects make it possible to perform operations that would otherwise be prohibited (e.g., deallocating an object) or to ensure that some obligation will be met (e.g., an opened file will be closed). However, different languages provide different interpretations of "uniqueness" and have different rules regarding how unique objects interact with the rest of the language. Our goal is to establish a common model that supports each of these languages, by allowing us to encode and study the interactions of the different forms of uniqueness. The model we provide is based on a substructural variant of the polymorphic -calculus, augmented with four kinds of mutable references: unrestricted, relevant, affine, and linear. The language has a natural operational semantics that supports deallocation of references, strong (t...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Amal J. Ahmed, Matthew Fluet, Greg Morrisett
• Keywords: ICFP 2005, Keywords Substructural Type, Mutable References, Programming Languages, Unique Objects