Functional Translation of a Calculus of Capabilities

Typing the memory state using capabilities

In the beginning my thesis, I developed with François Pottier a type system based on capabilities. This type system enables one to describe very precisely the memory state, and to control access to individual memory cells or groups of memory cells. Our type system extends System F by combining and generalizing several techniques:

capabilities, which describe the ownership of a piece of state (Crary, Walker and Morrisett, 1999),
singleton types, which help relating the type of a pointer with its associated memory cell (Smith, Walker and Morrisett, 2000),
adoption and focus, a mechanism which enables reasoning about data structures with sharing (Fähndrich and DeLine, 2002),
the frame rule, which can be used to focus the analysis on the memory cells that might actually get used in a piece of code (O'Hearn, Reynolds and Yang, 2001),
recursive ownership, which consists in associating a type to each capability and using this type to control the memory footprint covered by this capability; this is a key ingredient that we have introduced.

The development of this type system was motivated by the verification of imperative programs. Many ideas from this type system were indeed reused in my later work on CFML, where capabilities become Coq predicates over heaps. A capability-based type system might also have other interesting applications. In particular,

the fine-grained types of this system can be used to assign interfaces to mutable data structures that are more precise than if expressed using only Caml-style types; such more precise types make it more explicit how data structures should or should not be used;
compiler optimizations could take advantage of the non-aliasing information captured by types for reordering accesses to disjoint memory locations, or for automatically parallelizing non-interfering portions of code.

Publication

This work started from the intuition that if one is able to describe in a fine-grained way the ownership of pieces of state using capabilities, then one should be able to translate imperative programs into equivalent purely-functional programs in a systematic manner. Turning this intuition into a type system and a type-directed translation took quite some effort. The integration of all the features mentioned earlier on results in a very expressive, yet also fairly technical, type system. The complexity nevertheless seems to be inherent to the problem tackled: the coexistence of mutable states with higher-order functions is known to be particularly tricky to handle.

Functional Translation of a Calculus of Capabilities

Arthur Charguéraud and François Pottier

ICFP: International Conference on Functional Programming, September 2008

paper - abstract - appendix - slides - more

Follow-up work

This type system with capabilities was not meant to be directly implemented in a practical programming language, but rather to serve as a theoretical foundation upon which to develop other systems, possibly more practically-oriented ones. François Pottier and Jonathan Protzenko are currently working on adaptation of capabilities to a user-level type system for ML (2013).

François Pottier extended the system with the antiframe rule in order to add support for hidden state (2008). He developed a complete Coq formalization of this extended system (2011). Together with Alexandre Pilkiewicz, he adapted the type system to time complexity analysis (2011). Furthermore, Schwinghammer, Birkedal and Stovring have developed a Kripke model for our type system using ultra-metric spaces (2011).