[cap-talk] Backwater: some small progress

[Toby Murray]

On Sat, 2007-04-28 at 22:58 -0700, Mark S. Miller wrote:
> I know that Fred, in his search for a good formalism for reasoning about 
> authority, spent some time examining Pi Calculus before deciding to base SCOLL 
> on take-grant systems. Also, Toby Murray's 
> <http://web.comlab.ox.ac.uk/oucl/work/toby.murray/analysing_authority.pdf> 

Now see
http://web.comlab.ox.ac.uk/oucl/work/toby.murray/papers/analysing_authority.pdf

I'll have to look into the pi-calculus semantics sometime to see how
easily my work can be applied to Pict code. That would be a cool thing
indeed. Backwater appears to be the perfect "real world" target domain
for my work in the short term, since it's correspondence to a process
algebra so so strong and it is being used to build "real world" stuff
right now.

Awesome work Matej, btw.

> uses another process algebra, CSP, to reason about authority. (I have easily 
> understood Occam and Orc, and I have briefly understood Pict, but I don't 
> understand CSP. I'm not sure why some simple process algebras seem so much 
> easier to understand than others.)

Feel free to send CSP questions my way and I'll try to answer as best I
can. Bill Roscoe's definitive CSP book is also online at:
http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf

The first couple chapters give a good guide to CSP overall.