From: L.G. Meredith <lgreg.meredith@gmail.com>

Date: Wed, 2 Aug 2006 07:41:04 -0700

Message-ID: <5de3f5ca0608020741i124868c1ne802260fc872e9b1@mail.gmail.com>

To: "Marco Carbone" <carbonem@dcs.qmul.ac.uk>

Cc: "Steve Ross-Talbot" <steve@pi4tech.com>, "WS-Choreography List" <public-ws-chor@w3.org>

Date: Wed, 2 Aug 2006 07:41:04 -0700

Message-ID: <5de3f5ca0608020741i124868c1ne802260fc872e9b1@mail.gmail.com>

To: "Marco Carbone" <carbonem@dcs.qmul.ac.uk>

Cc: "Steve Ross-Talbot" <steve@pi4tech.com>, "WS-Choreography List" <public-ws-chor@w3.org>

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.3740Received on Wednesday, 2 August 2006 14:41:22 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Saturday, 18 December 2010 01:01:46 GMT
*