On asynchrony in name-passing calculi.

*(English)*Zbl 1093.68026Summary: 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.

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.