A Step-Index Model of Substructural State

• icfp05.pdf (with Amal Ahmed and Greg Morrisett; Appeared at ICFP'05; 20050926-ICFP05.ppt)

  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 lambda-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 (type-varying) updates, and storage of unique objects in shared references. We establish the strong soundness of the type system by constructing a novel, semantic interpretation of the types.

• techrpt.pdf (with Amal Ahmed and Greg Morrisett; Harvard University Technical Report; TR-16-05)

  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 lambda-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 (type-varying) updates, and storage of unique objects in shared references. We establish the strong soundness of the type system by constructing a novel, semantic interpretation of the types.

  This technical report is really two documents in one: The first part is a paper appearing in the Tenth ACM SIGPLAN International Conference on Functional Programming (ICFP'05). The second part is a formal development of the language, step-indexed model, and soundness proof referenced in the first part. If you have already read a version of "A Step-Indexed Model of Substructural State", then you should proceed directly to the appendices.

• 20050225-NEPLS.ppt (Presentation at the New England Programming Languages and Systems Symposium Series (NEPLS))

  Programming languages such as Clean, CQual, Cyclone, TAL, and Vault combine imperative features with some form of ``unique'' typing in order to refine the set of expressions that should be allowed (e.g., recycling a reference to hold values of a different type) or dis-allowed (e.g., failing to de-allocate a reference.) However, these languages provide different interpretations of ``uniqueness'' and have different rules regarding how unique values may be mixed with unrestricted constructors. Our goal is to provide a single model that allows us to express and evaluate the different interpretations and to study their interactions. To this end, we present a substructural polymorphic lambda-calculus with mutable references that includes four flavors of references (unrestricted, relevant, affine, and linear). This yields a rich design space, for which some questions have no ``right'' answer (e.g., should an unrestricted reference be allowed to hold an affine value?). We explore a scenario that is faithful to the operational interpretation of substructural logic, and also allows shared references to hold unique values (i.e., answering ``yes'' above) as well as strong (type-varying) updates on unique references. Our type system provides for controlled interaction among the different flavors of references and is justified by a standard operational semantics coupled with a step-indexed interpretation of types.