[Prev][Next][Index][Thread]
Two papers on the pi-calculus.
Dear colleagues,
I have been working, together with Martin Berger
and Nobuko Yoshida, on new type structures for the
pi-calculus. One of our aims is to capture, as precisely
as possible, the fruits of the study of typed lambda-calculi
in typed pi-calculi. Interaction with game semantics
plays an important role in this enterprise.
While our work so far, some of which we announce
here, is just the beginning, we hope it will open new
ways to use this calculus for the study of types of
programming languages and computation.
All best wishes,
Kohei Honda
Queen Mary, University of London
---------------------------------------
[1st Paper]
Title: Sequentiality and the Pi-Calculus
(available as: 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 games
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.