Lambda the Ultimate

Sophia Drossopolou, Greg Meredith, and I have written a paper demonstrating that we can use Caires' behavioral-spatial types to write security policies for objects in an ocap-secure language; then it's possible for the compiler to statically check that the implementation satisfies the policy. In an object capability language, dependency injection is the only way you get access to any ability to side-effect the world; all authority is embodied in object references, which are unforgeable. To deny someone the ability to perform an action, you simply do not give them a reference to the object that performs it. We focused on demonstrating that we can type deniability in the paper.

Lucius G Meredith, Mike Stay, Sophia Drossopoulou, "Policy as Types".

Greg and I are currently seeking crowdfunding to build a platform called splicious; should we get funded, part of our plan is to port the spatial logic model checker to Scala and add spatial-behavioral types as annotations with a plugin.