Re: Formal semantics paper - from Marco Carbone et al

Well may be I would add further words.  Marco's point of saying "loose"
is that Kobayashi-Igarashi-Rehof's method does not assume specific
syntactic constructs in description: it is for general pi-calculus 
processes.
The notion of session (usually realised by corelation identities or nonces
in web services) is based on explicit syntactic constructs for threading
communications in processes. This is why its type checking is immediate
in spite of rich type structure it can infer and it is why it can be 
used for
other diverse static and dynamic analyses.

kohei

Marco Carbone wrote:
>
>>> types are related to this but Kobayashi's are much more powerful and
>>> lose.
>>>
>>
>> I do not understand what "lose" means, anyway the main difference 
>> between
>
>
> Sorry, I forgot an 'o', I meant loose ;-)
>
>
>
>
>
>> Kobayashi-Igarashi's work and Rehof and others' work, are that theirs
>> are more about analysis of behaviour of processes than simple and basic
>> discipline for language constructs.
>>
>> For example if we have a function foobar in C or Java:
>>
>> (*)     int foobar(int i) {.....}
>>
>> then this is a simple typing, the signature, for a function. If we do 
>> not
>> have it, we lose a lot of ability to do ---- well almost anything. On 
>> the
>> top of this, and using this signature, we can do behavioural analysis of
>> programs.
>>
>> In the same way, session types are conceived as a basic type discipline
>> for communication behaviour. As such, it is
>>
>> (1) very easy to type check.
>> (2) essentially transparent to the programmer (like (*) above)
>> (3) faciliates and empowers diverse and richer analysis of descriptions
>> on the top of it.
>>
>> I in particular wish to emphasise the point (3). By having a basic
>> syntactic type structure in descriptions (or more simply put, by
>> enunciating each series of conversations  as such), we can perform
>> diverse validations on description very easily. This starts from
>> the standard monitoring to conformance to various consistency
>> checks to Kobayashi-Igarashi-Rehof's type/model checking tecniques
>> to security checks to logics.  (I remember this point was illustrated
>> by Steve's ACM Queue interview, though I have forgotten exact
>> wording.)
>>
>> Some of such derived analysis techniques will be formalised and
>> implemented into pi4soa tool in due course. The main point is
>> session typing offers a simple basis which amplifies the power
>> of other analyses. It was from the first conceived as such (in
>> 1994), and this aspect is being realised now.
>>
>> I thank Greg for putting forward this connection.
>>
>> Best wishes,
>>
>> kohei
>>
>>
>>
>>
>>
>
> ---------------------------------------------------------
> 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
> ---------------------------------------------------------
>
>

Received on Wednesday, 2 August 2006 14:42:41 UTC