Abstract:

Type systems are playing an increasingly important role in the theory of distributed systems. 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. In this paper, we study the impact of polymorphism on the algebraic theory of the 〖WTBX〗π〖WTBZ〗calculus. Precisely, we give an axiomatisation of the polymorphic 〖WTBX〗π〖WTBZ〗calculus, which is both sound and complete on the closed finite terms.

Key words: πcalculus；type system；polymorphism；bisimulation；axiomatisation