Re: Formal semantics paper - from Marco Carbone et al

> This looks like a lot of work. i may be misreading, because i have  
> only skimmed, but it looks as though the main theorem is a subject  
> reduction-like theorem in which the subject reduction is simulation- 
> style (ala Kobayashi's type systems) as opposed to a static subject  
> reduction (ala Honda, et al's type systems). Have you seen,  
> therefore, Kobayashi's 2006 types for concurrency paper (


Just to clarify, the paper has three main theorems:

1) Subject Reduction for the global calculus type system (session  
types) i.e. when the system evolves it is still well typed (e.g. I  
evolves to I' and I is well typed then also I' is well typed.

2) Subject Reduction for the end-point calculus (similar to point 1)

3) EPP Theorem, i.e.
	a) Type Preservation i.e. a well typed global description is  
projected to a well typed global interaction.
	b) Completeness i.e. if a global interaction I evolves to I' then  
its projection evolves to the "projection" of I' (EPP(I') )
	c) Soundness i.e. if a projection EPP ( I ) evolves to N then I can  
evolve to I' and the projection of I' is "similar" to N

1) and 2) guarantee that working with typed programs is safe (you  
never evolve to untyped i.e. unwanted things).

3) shows that given a global description (e.g. a WS-CDL  
choreography), its end-point projection is good and respects what the  
programmer wanted to specify in the choreography.

Hope this clarifies the key points of the paper.

Best,
Marco

P.S.
I didn't read the paper you linked but I believe it is related with  
another of his works i.e. having CCS processes as types. Session  
types are related to this but Kobayashi's are much more powerful and  
lose.




> http://www.kb.ecei.tohoku.ac.jp/~koba/papers/concur2006-full.pdf)?
>
> Best wishes,
>
> --greg
>
> On 8/1/06, Steve Ross-Talbot <steve@pi4tech.com> wrote:
>
> Is at:
>
> http://lists.w3.org/Archives/Public/www-archive/2006Aug/att-0000/
> workingNote.pdf
>
> Please read and comment as soon as possible.
>
> Cheers
>
> Steve T
>
>
>
>
> -- 
> L.G. Meredith
> Partner
> Biosimilarity LLC
> 505 N 72nd St
> Seattle, WA 98103
>
> +1 206.650.3740

---------------------------------------------------------
Marco Carbone

Dept. of Computer Science
Queen Mary University of London
Mile End Road
E1 4NS London
United Kingdom

Phone: +44 (0) 207 882 3659
Fax:      +44 (0) 208 980 6533
email:   carbonem@dcs.qmul.ac.uk
home:   http://www.dcs.qmul.ac.uk/~carbonem
---------------------------------------------------------