Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-24T20:11:39.364Z Has data issue: false hasContentIssue false

On asynchrony in name-passing calculi

Published online by Cambridge University Press:  23 September 2004

MASSIMO MERRO
Affiliation:
University of Verona, Italy
DAVIDE SANGIORGI
Affiliation:
University of Bologna, Italy

Abstract

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.

Type
Paper
Copyright
2004 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

An extended abstract of this paper appeared in the Proceedings of the 25th International Colloquium on Automata, Languages and Programming, July 1998, Springer-Verlag Lecture Notes in Computer Science1443.