Lightweight Static Capabilities

We describe a modular programming style that harnesses modern type systems to verify safety conditions in practical systems. This style has three ingredients:(i)A compact kernel of trust that is specific to the problem domain.(ii)Unique names (capabilities) that confer rights and certify properties, so as to extend the trust from the kernel to the rest of the application.(iii)Static (type) proxies for dynamic values. We illustrate our approach using examples from the dependent-type literature, but our programs are written in Haskell and OCaml today, so our techniques are compatible with imperative code, native mutable arrays, and general recursion. The three ingredients of this programming style call for (1) an expressive core language, (2) higher-rank polymorphism, and (3) phantom types.