LIPIcs.CONCUR.2015.212.pdf
- Filesize: 464 kB
- 14 pages
Document
Howe's Method for Contextual Semantics
Authors
-
Part of:
Volume:
26th International Conference on Concurrency Theory (CONCUR 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-08-26
Cite As Get BibTex
Serguei Lenglet and Alan Schmitt. Howe's Method for Contextual Semantics. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 212-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.212
Abstract
We show how to use Howe's method to prove that context bisimilarity is a congruence for process calculi equipped with their usual semantics. We apply the method to two extensions of HOpi, with passivation and with join patterns, illustrating different proof techniques.
Subject Classification
Keywords
- Bisimulation
- process calculi
- Howe's method
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Michael Baldamus and Thomas Frauenstein. Congruence proofs for weak bisimulation equivalences on higher-order process calculi. Technical report, Berlin University of Technology, 1995.
-
Giuseppe Castagna, Jan Vitek, and Francesco Zappa Nardelli. The Seal Calculus. Information and Computation, 201(1):1-54, 2005.
-
Cédric Fournet and Georges Gonthier. The reflexive cham and the join-calculus. In POPL'96, pages 372-385. ACM Press, 1996.
-
Cédric Fournet and Cosimo Laneve. Bisimulations in the join-calculus. Theorectical Computer Science, 266(1-2):569-603, 2001.
-
Jens C. Godskesen and Thomas Hildebrandt. Extending howe’s method to early bisimulations for typed mobile embedded resources with local names. In FSTTCS'05, volume 3821 of LNCS, pages 140-151. Springer, 2005.
-
Andrew D. Gordon. Bisimilarity as a theory of functional programming. Electronic Notes in Theoretical Computer Science, 1:232-252, 1995.
-
Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103-112, 1996.
-
Vasileios Koutavas and Matthew Hennessy. Symbolic bisimulation for a higher-order distributed language with passivation. In CONCUR'13, pages 167-181. Springer-Verlag, 2013.
-
Sergueï Lenglet. Bisimulations dans les calculs avec passivation. PhD thesis, Université de Grenoble, 2010.
-
Sergueï Lenglet and Alan Schmitt. Howe’s method for contextual semantics. Technical Report RR-8750, Inria, 2015.
-
Sergueï Lenglet, Alan Schmitt, and Jean-Bernard Stefani. Characterizing contextual equivalence in calculi with passivation. Information and Computation, 209(11):1390-1433, 2011.
-
Adrien Piérard and Eijiro Sumii. Sound bisimulations for higher-order distributed process calculus. In FOSSACS'11, volume 6604 of LNCS, pages 123-137. Springer, 2011.
-
Adrien Piérard and Eijiro Sumii. A higher-order distributed calculus with name creation. In LICS'12, pages 531-540. IEEE, 2012.
-
Davide Sangiorgi. Bisimulation for higher-order process calculi. Information and Computation, 131(2):141-178, 1996.
-
Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems, 33(1), 2011.
-
Davide Sangiorgi and David Walker. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001.
-
Alan Schmitt and Jean-Bernard Stefani. The Kell Calculus: A Family of Higher-Order Distributed Process Calculi. In Global Computing 2004 workshop, volume 3267 of LNCS, 2004.
-
Bent Thomsen. Plain chocs: A second generation calculus for higher order processes. Acta Informatica, 30(1):1-59, 1993.