A paper by Greg Meredith, Mike Stay and Sophia Drossopoulou page 
Of note:
- Meredith was the principal architect of Microsoft’s BizTalk. He is designer of Rholang
- Mike Stay worked at Google during his PhD . On category theory he concluded a new type system is required for programming distributed systems.
- Drossopoulou is a professor of CS at UCL. She builds on OCap i.e. capabilities-based-dom with Mark Miller.
> The object-capability (OCap) security model grew out of the realization that good object-oriented programming practice leads to good security properties. Separation of duties leads to separation of authority; information hiding leads to integrity; message passing leads to authorization; and dependency injection to authority injection. An OCap-secure programming language enforces these patterns: the only way an object can modify any state but its own is by sending messages on the object references it possesses. Authority can then be denied simply by not providing the relevant object reference. OCap languages do not provide ambient, undeniable authority such as the global variables in JavaScript, static mutable fields in Java and C#, or allowing access to arbitrary objects through pointer arithmetic as in C and C++.
Types of chess pieces, are beret policies in distributed board games (so we play on single board).
> We would like a way to declare the authority that an object ought to possess and then check whether the implementation matches the intent; that is, we would like a language for declaring security policy. Drossopoulou and Noble convincingly argue that none of the current specification methods adequately capture all of the capability policies required to support OCap systems. The most intriguing aspect of the capability policies proposed in is deniability. Deniability differs from usual style of specifications in the following two aspects: a) it describes policies which are open, i.e. apply to a module as well as all its extensions, and b) describes necessary conditions for some effect to take place. For example, a policy may require that in order for any piece of code to modify the balance of a bank account, it needs to have access to that account (access to the account is a necessary condition), and that this property is satisfied by all extensions of the account library (open). In contrast, classical Hoare Logic specifications describe sufficient conditions and are closed. In this paper we con- centrate on the use of the rho-calculus for ex- pressing deniability. To express necessary conditions, we invert the assertion and use bisimulation (e.g. any piece of code which does not have access to the ac- count will be bisimilar to code in which the balance of the account is not modified). To express openness, we adapt the concept of the adjoint to the separation operator, i.e. any further code P which is attached to the current code will be bisimilar to P in parallel with code which does not modify the balance of the account.
Curry-Howard sketch
In short, we show that the rho-calculus is an OCap language and sketch a translation from a subset of JavaScript into the calculus; we also demonstrate that the corresponding Hennessy-Milner logic suffices to capture the key notion of deniability. In the larger scheme, this identifies the notion of policy with the proposition-as-types paradigm, also known as The Curry-Howard isomorphism.