[e-lang] Formalising the notion of an object-capability language
toby.murray at comlab.ox.ac.uk
Fri Jan 22 11:47:23 PST 2010
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.
"Structural Operational Semantics for an Idealised Object-Capability
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
and use those to prove that Cajita is an object-capability language.
More information about the e-lang