The Plaid Language: Typed Core Specification (CMU-ISR-12-103)

Plaid is an object oriented programming language built on two paradigms. First, Plaid is typestateoriented. Programmers can directly encode the abstract states of objects and use the state change operator to change the state, interface, and representation of an object at runtime. Second, Plaid’s type system is permission-based. The type of each reference includes an access permission which dictates how the reference can be used and characterizes the permissions to other aliases of the same object. Plaid leverages permissions when tracking the abstract state of references during typechecking. Permissions are also used to infer code that can be safely run in parallel. This document defines the core of the Plaid language, including its source syntax, the semantics of operations involving abstract states, and a type system