We study Milner's encoding of the call-by-value -calculus into the π-calculus. We show that, by tuning the encoding to two subcalculi of the π-calculus (Internal π and Asynchronous Local π), the equivalence on -terms induced by the encoding coincides with Lassen's eager normal-form bisimilarity, extended to handle η-equality. As behavioural equivalence in the π-calculus we consider contextual equivalence and barbed congruence. We also extend the results to preorders. A crucial technical ingredient in the proofs is the recently-introduced technique of unique solutions of equations, further developed in this paper. In this respect, the paper also intends to be an extended case study on the applicability and expressiveness of the technique.

Durier, A., Hirschkoff, D., Sangiorgi, D. (2018). Eager functions as processes. N.Y. : Association for Computing Machinery [10.1145/3209108.3209152].

Eager functions as processes

Durier, Adrien;Sangiorgi, Davide
2018

Abstract

We study Milner's encoding of the call-by-value -calculus into the π-calculus. We show that, by tuning the encoding to two subcalculi of the π-calculus (Internal π and Asynchronous Local π), the equivalence on -terms induced by the encoding coincides with Lassen's eager normal-form bisimilarity, extended to handle η-equality. As behavioural equivalence in the π-calculus we consider contextual equivalence and barbed congruence. We also extend the results to preorders. A crucial technical ingredient in the proofs is the recently-introduced technique of unique solutions of equations, further developed in this paper. In this respect, the paper also intends to be an extended case study on the applicability and expressiveness of the technique.
2018
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18)
364
373
Durier, A., Hirschkoff, D., Sangiorgi, D. (2018). Eager functions as processes. N.Y. : Association for Computing Machinery [10.1145/3209108.3209152].
Durier, Adrien; Hirschkoff, Daniel; Sangiorgi, Davide
File in questo prodotto:
File Dimensione Formato  
lics_final_IRIS.pdf

accesso aperto

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 603.21 kB
Formato Adobe PDF
603.21 kB Adobe PDF Visualizza/Apri

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/11585/669217
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 3
social impact