zbMATH — the first resource for mathematics

Contextual equivalence for higher-order \(\pi\)-calculus revisited. (English) Zbl 1337.68185
Brookes, Steven (ed.), Proceedings of the 19th conference on mathematical foundations of programming semantics (MFPS XIX), Montreal, Canada, March 19–22, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 83, 149-168, electronic only (2003).
Summary: The higher-order \(\pi\)-calculus is an extension of the \(\pi\)-calculus to allow communication of abstractions of processes rather than names alone. It has been studied intensively by Sangiorgi in his thesis where a characterisation of a contextual equivalence for higher-order \(\pi\)-calculus is provided using labelled transition systems and normal bisimulations. Unfortunately the proof technique used there requires a restriction of the language to only allow finite types.
We revisit this calculus and offer an alternative presentation of the labelled transition system and a novel proof technique which allows us to provide a fully abstract characterisation of contextual equivalence using labelled transitions and bisimulations for higher-order \(\pi\)-calculus with recursive types also.
For the entire collection see [Zbl 1325.68013].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI