Functional translation of a calculus of capabilities

Abstract

Reasoning about imperative programs requires the ability to track aliasing and ownership properties. We present a type system that provides this ability, by using regions, capabilities, and singleton types. It is designed for a high-level calculus with higher-order functions, algebraic data structures, and references (mutable memory cells). The type system has polymorphism, yet does not require a value restriction, because capabilities act as explicit store typings.