Document Open Access Logo

Characteristic Bisimulation for Higher-Order Session Processes

Authors Dimitrios Kouzapas, Jorge A. Pérez, Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.398.pdf
  • Filesize: 0.58 MB
  • 14 pages

Document Identifiers

Author Details

Dimitrios Kouzapas
Jorge A. Pérez
Nobuko Yoshida

Cite As Get BibTex

Dimitrios Kouzapas, Jorge A. Pérez, and Nobuko Yoshida. Characteristic Bisimulation for Higher-Order Session Processes. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 398-411, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.398

Abstract

Characterising contextual equivalence is a long-standing issue for higher-order (process) languages. In the setting of a higher-order pi-calculus with sessions, we develop characteristic bisimilarity, a typed bisimilarity which fully characterises contextual equivalence. To our knowledge, ours is the first characterisation of its kind. Using simple values inhabiting (session) types, our approach distinguishes from untyped methods for characterising contextual equivalence in higher-order processes: we show that observing as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes. We demonstrate how characteristic bisimilarity can be used to justify optimisations in session protocols with mobile code communication.

Subject Classification

Keywords
  • Behavioural equivalences
  • session types
  • higher-order process calculi

Metrics

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

References

  1. Giovanni Bernardi, Ornela Dardha, Simon J. Gay, and Dimitrios Kouzapas. On duality relations for session types. In TGC 2014, volume 8902 of LNCS, pages 51-66. Springer, 2014. Google Scholar
  2. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. Google Scholar
  3. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In ESOP'98, volume 1381 of LNCS, pages 22-138, 1998. Google Scholar
  4. Kohei Honda and Nobuko Yoshida. On reduction-based process semantics. TCS, 151(2):437-486, 1995. Google Scholar
  5. Alan Jeffrey and Julian Rathke. Contextual equivalence for higher-order pi-calculus revisited. LMCS, 1(1), 2005. Google Scholar
  6. Vasileios Koutavas and Matthew Hennessy. First-order reasoning for higher-order concurrency. Computer Languages, Systems & Structures, 38(3):242-277, 2012. Google Scholar
  7. Dimitrios Kouzapas. Full version of this paper, 2015. URL: http://arxiv.org/abs/1502.02585.
  8. Dimitrios Kouzapas and Nobuko Yoshida. Globally governed session semantics. LMCS, 10(4), 2014. Google Scholar
  9. Dimitrios Kouzapas, Nobuko Yoshida, Raymond Hu, and Kohei Honda. On asynchronous eventful session semantics. MSCS, 2015. Google Scholar
  10. Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi, and Alan Schmitt. On the expressiveness and decidability of higher-order process calculi. Inf. Comput., 209(2):198-226, 2011. Google Scholar
  11. Robin Milner and Davide Sangiorgi. Barbed bisimulation. In W. Kuich, editor, 19th ICALP, volume 623 of LNCS, pages 685-695. Springer, 1992. Google Scholar
  12. Dimitris Mostrous and Nobuko Yoshida. Two session typing systems for higher-order mobile processes. In TLCA, volume 4583 of LNCS, pages 321-335. Springer, 2007. Google Scholar
  13. Dimitris Mostrous and Nobuko Yoshida. Session typing and asynchronous subtyping for the higher-order π-calculus. Inf. Comput., 241:227-263, 2015. Google Scholar
  14. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput., 239:254-302, 2014. Google Scholar
  15. Davide Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher Order Paradigms. PhD thesis, University of Edinburgh, 1992. Google Scholar
  16. Davide Sangiorgi. Bisimulation for Higher-Order Process Calculi. Inf. & Comp., 131(2):141-178, 1996. Google Scholar
  17. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. In LICS, pages 293-302. IEEE, 2007. 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