Formalising the notion of an object-capability language

Dear e-langers,

Folks on this list might be interested in the following paper and MSc
thesis I came across today.

The author develops a minimal object-capability language called
"Class", gives it a formal operational semantics and using those
semantics proves that the language adheres to the object-capability
model, i.e. that it is in-fact an object-capability language.

P. Dinges
"Structural Operational Semantics for an Idealised Object-Capability
Programming Language"

http://www.elwedgo.de/en/portfolio/theses/class-language.html

The main theorem proved is that "user objects can contain references
only from arguments of received messages and from return values of
sent messages", where the instruction to create a new object is
considered as a kind of message send.

I haven't dug into this, but it does look interesting.

This kind of thing looks particularly relevant to the Caja folks who
might consider how could take pre-existing semantics for JavaScript
and use those to prove that Cajita is an object-capability language.

Cheers

Toby