[TYPES] Genericity and the Pi-Calculus

[Martin Berger]

Dear colleagues,

Kohei Honda, Nobuko Yoshida and myself would like to announce our
paper

    Genericity and the Pi-Calculus.

It is available from

   http://www.dcs.qmul.ac.uk/~martinb/publications/genericity-full.ps.gz
   http://www.dcs.qmul.ac.uk/~martinb/publications/genericity-full.pdf

We hope it is of interest to you and would greatly appreciate your
comments.

Martin


PS: here's the abstract.

Types in processes delineate specific classes of interactive behaviour
in a compositional way. Key elements of process theory, in particular
behavioural equivalences, are deeply affected by types, leading to
applications in the descriptions and analyses of diverse forms of
computing. As one of the examples of types for processes, this paper
introduces a second-order polymorphic pi-calculus based on duality
principles, building on type structures coming from typed pi-calculi,
Linear Logic and game semantics. The calculus cleanly captures the
main technical achievements of earlier work on second-order
polymorphism, allowing a precise embedding of generic sequential
functions possible as well as seamless integration with state and
concurrency. In this paper, we study the linear polymorphic type
discipline, the most basic form of duality-based
polymorphism. Representing a class of strongly normalising polymorphic
interaction, it allows us to illustrate various elements of the theory
in a simple setting. A corresponding behavioural theory of polymorphic
labelled transitions is studied, strengthening Pierce-Sangiorgi's
polymorphic bisimulation via duality. As an application we give a
fully abstract embedding of System F in the polymorphic
pi-calculus. The proof combines process-theoretic reasoning with
techniques from game semantics. The abstract nature of our generic
(polymorphic) labelled transitions plays an essential role,
elucidating subtle aspects of polymorphism in functions and
interaction.