On asynchrony in name-passing calculi

The asynchronous pi-calculus is considered the basis of experimental programming languages (or proposal of programming languages) like Pict, Join, and TyCO. However, at acloser inspection, these languages are based on an even simpler calculus, called Localised pi (Lpi), 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 Lpi. We focus on bisimulation-based behavioural equivalences, precisely on barbed congruence. We prove two coinductive characterisations of barbed congruence in Lpi, 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.