[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.