Lightweight Static Capabilities
Oleg Kiselyov, Chung-chieh Shan · Electronic Notes in Theoretical Computer Science · 2007
We describe a modular programming style that harnesses modern type systems to verify safety conditions in practical systems. This style has three ingredients: A compact kernel of trust that is specific to the problem domain. Unique names (capabilities) that confer rights and certify properties, so as to extend the trust from the kernel to the rest of the application. Static (type) proxies for dynamic values.