Re: Formal semantics paper - from Marco Carbone et al

>> 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 13:36:47 UTC