[Prev][Next][Index][Thread]
paper on polymorphic pi-calculus available
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The paper below is now availabile at
http://www.cs.indiana.edu/hyplan/pierce/ftp/polybisim.ps.gz
or
ftp://ftp.dcs.ed.ac.uk/pub/sad/poly.ps.gz
Best regards,
Benjamin Pierce
Davide Sangiorgi
***********
Title: Behavioral Equivalence in the Polymorphic Pi-Calculus
Authors: Benjamin Pierce and Davide Sangiorgi
note: To appear as Indiana University Computer Science Technical
Report TR 468 and as an INRIA Technical Report.
Abstract: We investigate parametric polymorphism in message-based concurrent
programs, 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.