Two papers on the pi-calculus.

[Kohei Honda <kohei@xxxxxxxxxxxxx>]

Dear colleagues,

Martin, Nobuko and I have been working on type
structures for the pi-calculus. Our aim is to
prepare the pi-calculus as a basic tool for
the precise representation of computation.
This involves new notions of types, new notions
of behavioural equality, and a new understanding
on syntax, all on the basis of the study on the
calculus for the last 10 years, including its
connection to game semantics.

Our experience seems to suggest the best fruits
from the traditional semantic study (largely
centering on the idea of higher-order functions)
can be precisely captured and unified in the
context of the pi-calculus.

Here I wish to report the completion of full
versions of the two papers in this project, which
laid a basis of our ongoing study.  I wish these
work can be used for opening further possibilities
of both foundational studies and applications.

Best wishes,

kohei
[originally submitted on August 13, 2001]

----------------------------------------------
Subsequent work can be found in our web pages.
At appropriate moments they will be announced
in mailing lists and by other means.
----------------------------------------------

[1st Paper]

Title: Sequentiality and the Pi-Calculus

(available at: ftp://ftp.dcs.qmul.ac.uk/lfp/martinb/tlca01-full.ps.gz)

Extended Abstract appeared in Proc. of TLCA 2001,
the 5th International Conference on Typed Lambda
Calculi and Applications, LNCS 2044, pp.29-45,
Springer-Verlag, May 2001.

[Abstract]
We present a type discipline for the pi-calculus which precisely
captures the notion of sequential functional computation as a specific
class of name passing interactive behaviour. The typed calculus allows
direct interpretation of both call-by-name and call-by-value
sequential functions. The precision of the representation is
demonstrated by way of a fully abstract encoding of PCF. The result
shows how a typed pi-calculus can be used as a descriptive tool for
a significant class of programming languages without losing the
latter's semantic properties.  Close correspondence with game semantics
and process-theoretic reasoning techniques are together used to
establish full abstraction.

----------------------------------------------

[2nd Paper]

Strong Normalisation in the Pi-Calculus

(available at: http://www.mcs.le.ac.uk/~nyoshida/paper.html)

Extended Abstract appeared in Proc. LICS'01,
the 16th Annual IEEE Symposium on Logic and
Computer Science, pp.311-322, IEEE, June, 2001.

We introduce a typed pi-calculus where strong normalisation is
ensured by typability.  Strong normalisation is a useful property
in many computational contexts, including distributed systems. In
spite of its simplicity, our type discipline captures a wide
class of converging name-passing interactive behaviour. The proof
of strong normalisability combines methods from typed
lambda-calculi and linear logic with process-theoretic reasoning.
It is adaptable to systems involving state and other
extensions. Strong normalisation is shown to have significant
consequences, including finite axiomatisation of weak
bisimilarity, a fully abstract embedding of the simply-typed
lambda-calculus with products and sums and basic liveness in
interaction.

Strong normalisability has been extensively studied as a
fundamental property in functional calculi, term rewriting and
logical systems. This work is one of the first steps to extend
theories and proof methods for strong normalisability to the
context of name-passing processes.



  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html