Re: Formal semantics paper - from Marco Carbone et al

Marco, Kohei,

Thanks for clarifying. i was refering to the EPP theorem on page 85, which i
took as the central result of the work. Sorry, if i was a bit eliptical. My
thought was that the end point calculus is actually a type system and end
point projection was like the calculation of a kind of minimal type. Then,
you can see the EPP theorem in the light of subject reduction.

i know that you have a separate notion of typing laid out in the paper, but
i tend to think -- much in the way Kohei laid out -- of towers of typing of
increasing strength. Abramsky gives a good example of such in his
Marktoberdorff lecture with Simon Gay and Raja Nagaranjan on types for
concurrency.

That said, i was trying to draw an analogy between the EPP and Kobayashi's
usages. More specifically, in my mind there is connection between the fact
that EPP is a function and Kobayashi has a type inference algorithm -- apart
from the practical implication that the programmer doesn't have to write the
type.

Best wishes,

--greg

On 8/2/06, Marco Carbone <carbonem@dcs.qmul.ac.uk> wrote:
>
> 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<http://www.kb.ecei.tohoku.ac.jp/%7Ekoba/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<http://www.dcs.qmul.ac.uk/%7Ecarbonem>
> ---------------------------------------------------------
>
>


-- 
L.G. Meredith
Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103

+1 206.650.3740