The π-calculus is used as a model for programming languages. Its cons exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined cons are expected.In this paper we focus on two such common disciplines: sequentiality, meaning that at any time there is a single thread of computation, and well-bracketing, meaning that calls to external services obey a stack-like discipline. We formalise the disciplines by means of type systems. The main focus of the paper is on studying the consequence of the disciplines on behavioural equivalence. We define and study labelled bisimilarities for sequentiality and well-bracketing. These relations are coarser than ordinary bisimilarity. We prove that they are sound for the respective (conual) barbed equivalence, and also complete under a certain technical condition.We show the usefulness of our techniques on a number of examples, that have mainly to do with the representation of functions and store.

Hirschkoff D., Prebet E., Sangiorgi D. (2021). On sequentiality and well-bracketing in the π-calculus. N.Y. : Institute of Electrical and Electronics Engineers Inc. [10.1109/LICS52264.2021.9470559].

On sequentiality and well-bracketing in the π-calculus

Prebet E.;Sangiorgi D.
2021

Abstract

The π-calculus is used as a model for programming languages. Its cons exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined cons are expected.In this paper we focus on two such common disciplines: sequentiality, meaning that at any time there is a single thread of computation, and well-bracketing, meaning that calls to external services obey a stack-like discipline. We formalise the disciplines by means of type systems. The main focus of the paper is on studying the consequence of the disciplines on behavioural equivalence. We define and study labelled bisimilarities for sequentiality and well-bracketing. These relations are coarser than ordinary bisimilarity. We prove that they are sound for the respective (conual) barbed equivalence, and also complete under a certain technical condition.We show the usefulness of our techniques on a number of examples, that have mainly to do with the representation of functions and store.
2021
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '21)
1
13
Hirschkoff D., Prebet E., Sangiorgi D. (2021). On sequentiality and well-bracketing in the π-calculus. N.Y. : Institute of Electrical and Electronics Engineers Inc. [10.1109/LICS52264.2021.9470559].
Hirschkoff D.; Prebet E.; Sangiorgi D.
File in questo prodotto:
File Dimensione Formato  
LICS_iris.pdf

accesso aperto

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 391.51 kB
Formato Adobe PDF
391.51 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/851822
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact