Document Open Access Logo

On the Representation of References in the Pi-Calculus

Authors Daniel Hirschkoff, Enguerrand Prebet, Davide Sangiorgi

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.34.pdf
  • Filesize: 0.53 MB
  • 20 pages

Document Identifiers

Author Details

Daniel Hirschkoff
  • ENS de Lyon, France
Enguerrand Prebet
  • ENS de Lyon, France
Davide Sangiorgi
  • Università di Bologna, Italy
  • INRIA, Sophia Antipolis, France

Funding

Hirschkoff and Prebet acknowledge support from the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157), and from LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d’Avenir" ANR-11-IDEX-0007. Sangiorgi acknowledges support from the MIUR-PRIN project "Analysis of Program Analyses" (ASPRA, ID: 201784YSZ5_004), and from the European Research Council (ERC) Grant DLV-818616 DIAPASoN.

Cite As Get BibTex

Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On the Representation of References in the Pi-Calculus. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.34

Abstract

The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). While translations of references in π-calculi (and CCS) have appeared, the precision of such translations has not been fully investigated. In this paper we address this issue.
We focus on the asynchronous π-calculus (Aπ), where translations of references are simpler. We first define π^ref, an extension of Aπ with references and operators to manipulate them, and illustrate examples of the subtleties of behavioural equivalence in π^ref. We then consider a translation of π^ref into Aπ. References of π^ref are mapped onto names of Aπ belonging to a dedicated "reference" type. We show how the presence of reference names affects the definition of barbed congruence. We establish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in the two calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms of labelled bisimilarities. For one bisimilarity we derive both soundness and completeness; for another, more efficient and involving an inductive "game" on reference names, we derive soundness, leaving completeness open. Finally, we discuss examples of uses of the bisimilarities.

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
Keywords
  • Process calculus
  • Bisimulation
  • Asynchrony
  • Imperative programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. R. M. Amadio, I. Castellani, and D. Sangiorgi. On bisimulations for the asynchronous pi-calculus. Theor. Comput. Sci., 195(2):291-324, 1998. Google Scholar
  2. F. Bonchi, D. Petrişan, D. Pous, and J. Rot. A general account of coinduction up-to. Acta Informatica, pages 1-64, 2016. Google Scholar
  3. S. D. Brookes. The Essence of Parallel Algol. Inf. Comput., 179(1):118-149, 2002. Google Scholar
  4. S. Castellan, P. Clairambault, J. Hayman, and G. Winskel. Non-angelic concurrent game semantics. In Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, pages 3-19, 2018. Google Scholar
  5. M. Coppo, M. Dezani-Ciancaglini, N. Yoshida, and L. Padovani. Global progress for dynamically interleaved multiparty sessions. Math. Struct. Comput. Sci., 26(2):238-302, 2016. Google Scholar
  6. M. P. Fiore, E. Moggi, and D. Sangiorgi. A fully abstract model for the π-calculus. Inf. Comput., 179(1):76-117, 2002. Google Scholar
  7. M. Hennessy. A distributed Pi-calculus. Cambridge University Press, 2007. Google Scholar
  8. M. P. Herlihy. Impossibility and universality results for wait-free synchronization. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, PODC '88, pages 276-290, 1988. Google Scholar
  9. D. Hirschkoff, E. Prebet, and D. Sangiorgi. Online appendix to this paper. available from https://hal.archives-ouvertes.fr/hal-02895654, 2020. Google Scholar
  10. C.-K. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and kripke logical relations. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pages 59-72, 2012. Google Scholar
  11. G. Jaber and N. Tzevelekos. Trace semantics for polymorphic references. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 585-594, 2016. Google Scholar
  12. B. Jacobs. Introduction to coalgebra. towards mathematics of states and observations. Draft, 2014. Google Scholar
  13. N. Kobayashi. A partially deadlock-free typed process calculus. Transactions on Programming Languages and Systems, 20(2):436-482, 1998. A preliminary version in 12th Lics Conf. IEEE Computer Society Press 128-139, 1997. Google Scholar
  14. M. Merro, J. Kleist, and U. Nestmann. Mobile objects as mobile processes. Information and Computation, 177(2):195-241, 2002. Google Scholar
  15. R. Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  16. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, (Parts I and II). Inf. Comput., 100:1-77, 1992. Google Scholar
  17. A. S. Murawski and N. Tzevelekos. Full abstraction for reduced ML. Ann. Pure Appl. Logic, 164(11):1118-1143, 2013. Google Scholar
  18. D. Pous and D. Sangiorgi. Advanced Topics in Bisimulation and Coinduction (D. Sangiorgi and J. Rutten editors), chapter Enhancements of the coinductive proof method. Cambridge University Press, 2011. Google Scholar
  19. J. C. Reynolds. The essence of ALGOL. In Algorithmic Languages, pages 345-372. North-Holland, 1981. Google Scholar
  20. C. Röckl and D. Sangiorgi. A pi-calculus process semantics of concurrent idealised ALGOL. In Foundations of Software Science and Computation Structure, Second International Conference, FoSSaCS'99, volume 1578 of Lecture Notes in Computer Science, pages 306-321. Springer, 1999. Google Scholar
  21. J. Rot, F. Bonchi, M. M. Bonsangue, D. Pous, J. Rutten, and A. Silva. Enhanced coalgebraic bisimulation. Math. Struct. Comput. Sci., 27(7):1236-1264, 2017. Google Scholar
  22. D. Sangiorgi. The name discipline of uniform receptiveness. Theor. Comput. Sci., 221(1-2):457-493, 1999. Google Scholar
  23. D. Sangiorgi. Typed pi-calculus at work: A Correctness Proof of Jones’s Parallelisation Transformation on Concurrent Objects. TAPOS, 5(1):25-33, 1999. Google Scholar
  24. D. Sangiorgi and D. Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge university press, 2003. Google Scholar
  25. I. Stark. A fully abstract domain model for the pi-calculus. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 36-42. IEEE Computer Society, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact