Behavioral Equivalence in the Polymorphic Pi-calculus

We investigateparametric polymorphism in message-basedconcurrentprogramming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambdacalculus of Girard and Reynolds. Polymorphism constrains the power of observers by preventing them from directly manipuata 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 examconcurrent 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.

• Type: Conference
• Year: 1997
• Where: POPL
• Authors: Benjamin C. Pierce, Davide Sangiorgi
• Keywords: Investigateparametric Polymorphism, Polymorphic Lambdacalculus, POPL 1997, Programming Languages, Typed Process Calculus