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

On Mon, Jul 8, 2013 at 6:08 AM, Drossopoulou, Sophia <
s.drossopoulou-AQ/[email protected]> wrote:

>  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****
>
> **
>

Hi Sophia, what's the diference between slides 28 and 29? The change in
font size makes other changes hard to spot.



>  **
>
> 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?
>

I generally find that keeping more than one list in the addressees list is
bad, as replies from subscribers to one list are not seen by subscribers to
other lists. That's why my first message suggested "that further general
discussion should occur only on the e-lang list. (Subscribe at <
http://www.eros-os.org/mailman/listinfo/e-lang>. You need to subscribe to
post.)"

By the same token, keeping a list + many individuals creates the same
problem. The e-lang list has been very quiet lately so I encourage everyone
here interested in this topic to subscribe (as Sophia has). After today, I
suggest we drop the other individual addressees and just continue this
thread on e-lang. (Also, the mailing list software flags messages with too
many addressees as needing administer approval, delaying their public
posting. So dropping the individual addressees will solve this as well.)



> ****
>
> ** **
>
> *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.****
>
> ** **
>



-- 
Text by me above is hereby placed in the public domain

  Cheers,
  --MarkM

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