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

Revised paper: Behavioral Equivalence in the Polymorphic Pi-Calculus



We are pleased to announce a revised and expanded version of our 1997
study of the polymorphic pi-calculus, available through:

     http://www.cis.upenn.edu/~bcpierce/papers/polybisim.ps.gz

For those familiar with earlier versions of this paper, the main
improvements are as follows:

  * a major new section on a labeled-bisimulation presentation of the
    polymorphic pi-calculus (the original paper developed only barbed
    bisimulation), and

  * a new section extending our observations on "information leakage"
    in calculi with both polymorphism and aliasing.  We show how
    the small examples in the original version of our paper can be
    extended to allow a form of ad-hoc overloading in ML. 

Regards,

     Benjamin Pierce
     Davide Sangiorgi

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

        BEHAVIORAL EQUIVALENCE IN THE POLYMORPHIC PI-CALCULUS

                Benjamin Pierce  and  Davide Sangiorgi

Abstract:

We investigate parametric polymorphism in message-based concurrent
programming, focusing on behavioral equivalences in a typed process
calculus analogous to the polymorphic lambda-calculus of Girard and
Reynolds.

Polymorphism constrains the power of observers by preventing them from
directly manipulating data values whose types are abstract, leading to
notions of equivalence much coarser than the standard untyped ones.
We study the nature of these constraints through simple examples of
concurrent abstract data types and develop basic theoretical machinery
for establishing bisimilarity of polymorphic processes.

We also observe some surprising interactions between polymorphism and
aliasing, drawing examples from both the polymorphic pi-calculus and
ML.