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:
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,
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.
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).