Lambda the Ultimate

(As seen posted on an Obj Cap list today)

Uniqueness and Reference Immutability for Safe Parallelism. 2012.

We provide a novel combination of im- mutable and unique (isolated) types that ensures safe paral- lelism (race freedom and deterministic execution). The type system includes support for polymorphism over type quali- fiers, and can easily create cycles of immutable objects. Key to the system’s flexibility is the ability to recover immutable or externally unique references after violating uniqueness without any explicit alias tracking. Our type system models a prototype extension to C# that is in active use by a Mi- crosoft team. We describe their experiences building large systems with this extension. We prove the soundness of the type system by an embedding into a program logic.