[Prev][Next][Index][Thread]

A paper on pi-calculus types.

Dear Colleagues, 

In this mail, I wish to inform you of the availability of
my recent work about types for the pi-calculus, titled:
``A theory of types for pi-calculus.'' It can be obtained
from the following addresses.

   http://www.dcs.qmw.ac.uk/~kohei
   ftp://ftp.dcs.qmw.ac.uk/lfp/kohei/pitype.ps.gz

In this work, whose central ideas come from Milner's early
manuscript, and which also uses suggestions from game-based
semantics and various type disciplines for name passing
processes, we present a semantic foundation of typed
pi-calculi with a few applications, as well as offering a
$\pi$-calculus viewpoint on games semantics.  The landscape
of process types, as viewed from the present theory, shows
an interesting difference from that of function types,
though the paradigm of the latter plays an essential role
in the development of the present theory.  I sincerely wish
that this work can be interesting to both those who are
interested in types for concurrency, especially in their
semantic aspects, and those with interests in the semantics
of computation based on intensional structures.

I attach below a summary of its possible technical
contributions, hoping they can give some ideas about its
content.

I will be most grateful if you can give me any comments
and criticisms on this work.

                           Best regards,

                           kohei 

PS: To those who happen to have older versions of the
paper, please see ptnote.ps.gz in the same directory for
changes from the preceding versions.

--------------------------------------------------------------
Summary of contributions.
--------------------------------------------------------------
Basic Theory:

-- A general notion of types for name passing interactions, 
   with a few concrete examples of types.
-- Basic study of algebra of early name passing synchronisation 
   trees, as the foundations of theory of types.
-- Two general classes of universes of types based on the above 
   algebra. These classes contain models of known typed 
   pi-calculi and many games universes.
-- The theory of inhabitation and, as its applications, 
   typed bisimilarities and behavioural subtyping. 

Applications:

-- Sound models of Milner's basic sorting and Pierce-Sangiorgi's 
   IO-subsorting. Both models involve non-trivial analysis 
   of sorted dynamics, including a semantic characterisation of
   syntactic subsorting.
-- A concise presentation of a simple games universe as theory
   of types for the pi-calculus. 

At the level of reasoning methods, the work may contain novelty
in a few presented, and used, co-inductive reasoning methods,
which often employ directed relations (i.e. not symmetric,
though not necessarily transitive); and in the incorporation of
partiality at the basic level of compositional reasoning of
processes.