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.

On asynchrony in name-passing calculi

MERRO, Massimo
;
2004-01-01

Abstract

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.
2004
Asynchronous systems; process calculus; mobility
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/302345
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 55
  • ???jsp.display-item.citation.isi??? 45
social impact