Re: Formal semantics paper - from Marco Carbone et al

Just to add a bit:

> 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.
>

I do not understand what "lose" means, anyway the main difference between
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

Received on Wednesday, 2 August 2006 12:31:15 UTC