Functional translation of a calculus of capabilities

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. We exhibit a type-directed, type-preserving, and meaningpreserving translation of this imperative calculus into a pure calculus. Like the monadic translation, this is a store-passing translation. Here, however, the store is partitioned into multiple fragments, which are threaded through a computation only if they are relevant to it. Furthermore, the decomposition of the store into fragments can evolve dynamically to reflect ownership transfers. The translation offers deep insight about the inner workings and soundness of t...

• Type: Conference
• Year: 2008
• Where: ICFP
• Authors: Arthur Charguéraud, François Pottier
• Keywords: ICFP 2008, Imperative Calculus, Imperative Programs, Imperative Source Calculus, Programming Languages