zbMATH — the first resource for mathematics

On asynchrony in name-passing calculi. (English) Zbl 1093.68026
Summary: The asynchronous \(\pi\)-calculus has been considered as the basis of experimental programming languages (or proposals for programming languages) like Pict, Join and TyCO. However, on closer inspection, these languages are based on an even simpler calculus, called Localised \(\pi\) (L\(\pi\)), where: (a) only the output capability of names may be transmitted; (b) there is no matching or similar constructs for testing equality between names.
We study the basic operational and algebraic theory of L\(\pi\). We focus on bisimulation-based behavioural equivalences, more precisely, on barbed congruence. We prove two coinductive characterisations of barbed congruence in L\(\pi\), and some basic algebraic laws. We then show applications of this theory, including: the derivability of the delayed input; the correctness of an optimisation of the encoding of call-by-name \(\lambda\)-calculus; the validity of some laws for Join; the soundness of Thielecke’s axiomatic semantics of the Continuation Passing Style calculus.

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI