Reasoning about Object Capabilities using Logical Relations and Effect Parametricity

All,

Since I think this is relevant for the object capabilities community,
I'd like to advertise a paper by Lars Birkedal, Frank Piessens and
myself in which we propose a new formal characterisation of object
capabilities. The main messages of the paper are:

* The "topology-only bound on authority" (as formalised by properties
like "no authority amplification" and "only connectivity begets
connectivity") is fundamentally insufficient for characterising
capability-safe languages and for reasoning about ocap code.

* We propose an alternative characterisation using recent reasoning
techniques from the programming languages research community as well
as some ideas of our own.

* We demonstrate how to reason (on paper) about some non-trivial examples.

* We show that our characterisation implies the topology-only bound on
authority.

* Capability-safety can be safely understood as grouping together
three (more or less independent) language features/properties:
  * standard encapsulation of private state (as present in many languages)
  * primitive effects only available through capabilities
  * no static mutable global state

If you want to take a closer look, the paper is available at:
  https://lirias.kuleuven.be/bitstream/123456789/529252/1/paper-preprint.pdf
The presentation I gave about the work here yesterday at the IEEE
EuroS&P conference is available too:
  https://people.cs.kuleuven.be/dominique.devriese/obj-cap-log-rel-eff-param.pdf
Technical details and proofs are available in an associated technical report:
  https://lirias.kuleuven.be/bitstream/123456789/524074/1/CW690.pdf

We welcome any comments, insights and questions that you may have.

Regards,
Dominique