Re: [Caja] Important new paper: The Need for Capability Policiies

Hi Mark,

Ø  From: Mark Miller [mailto:[email protected]]

Ø   … relevant to this is Matej Kosik's ocap taming of Benjamin Pierce's Pict Language: ….

Ø  … It would be interesting to see … A proof (or even informal argument) that the Pict implementation satisfies these types.

James and I have a sketch for a proof that the Joe code satisfies Pol_2. An interesting observation is that the proof makes use both of Hoare-logic-like specs and reasoning (sufficient conditions), and of type annotations like private and final (which are about “deny” properties). The sketch can be found in the slides from our talk at FtfJP’13 at pages 26-30. The slides are available from
          http://www.doc.ic.ac.uk/~scd/CAPE-FTfJP%2713_slides.pdf

Sophia

PS Does

Ø  [+kosik]

Ø  [-google-caja-discuss, -cap-talk] Use e-lang as the only list for further discussions.
mean that the only recipients of these messages should be e-lang? Should I not have copied the other recipients?

From: Mark Miller [mailto:[email protected]]
Sent: 07 July 2013 20:32
To: Discussion of E and other capability languages; Matej Kosik
Cc: Stephen Chong; Robert N. M. Watson; Toby Murray; Fred Spiessens; John Mitchell; Benjamin Pierce; Shriram Krishnamurthi; Joe Gibbs Politz; Arjun Guha; Gareth Smith; Gardner, Philippa A; Ankur Taly; David Wagner; Adrian Mettler; Ben Laurie; Jonathan Shapiro; M. Scott Doerrie; Drossopoulou, Sophia; James Noble; Gregory Meredith
Subject: Re: [Caja] Important new paper: The Need for Capability Policiies

[+kosik]
[-google-caja-discuss, -cap-talk] Use e-lang as the only list for further discussions.

Hi Mike, relevant to this is Matej Kosik's ocap taming of Benjamin Pierce's Pict Language:
http://www2.fiit.stuba.sk/~kosik/doc/sofsem2008.pdf
http://www2.fiit.stuba.sk/~kosik/doc/tamed-pict--standard-library.pdf

It would be interesting to see
* This concrete example coded in Tamed Pict,
* The specs from the position paper formally restated in these spatial and temporal types, and
* A proof (or even informal argument) that the Pict implementation satisfies these types.

_______________________________________________
e-lang mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/e-lang