Howe's Method for Contextual Semantics

Authors Serguei Lenglet, Alan Schmitt

Thumbnail PDF


  • Filesize: 464 kB
  • 14 pages

Document Identifiers

Author Details

Serguei Lenglet
Alan Schmitt

Cite AsGet 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)


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.
  • Bisimulation
  • process calculi
  • Howe's method


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


  1. Michael Baldamus and Thomas Frauenstein. Congruence proofs for weak bisimulation equivalences on higher-order process calculi. Technical report, Berlin University of Technology, 1995. Google Scholar
  2. Giuseppe Castagna, Jan Vitek, and Francesco Zappa Nardelli. The Seal Calculus. Information and Computation, 201(1):1-54, 2005. Google Scholar
  3. Cédric Fournet and Georges Gonthier. The reflexive cham and the join-calculus. In POPL'96, pages 372-385. ACM Press, 1996. Google Scholar
  4. Cédric Fournet and Cosimo Laneve. Bisimulations in the join-calculus. Theorectical Computer Science, 266(1-2):569-603, 2001. Google Scholar
  5. 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. Google Scholar
  6. Andrew D. Gordon. Bisimilarity as a theory of functional programming. Electronic Notes in Theoretical Computer Science, 1:232-252, 1995. Google Scholar
  7. Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103-112, 1996. Google Scholar
  8. Vasileios Koutavas and Matthew Hennessy. Symbolic bisimulation for a higher-order distributed language with passivation. In CONCUR'13, pages 167-181. Springer-Verlag, 2013. Google Scholar
  9. Sergueï Lenglet. Bisimulations dans les calculs avec passivation. PhD thesis, Université de Grenoble, 2010. Google Scholar
  10. Sergueï Lenglet and Alan Schmitt. Howe’s method for contextual semantics. Technical Report RR-8750, Inria, 2015. Google Scholar
  11. Sergueï Lenglet, Alan Schmitt, and Jean-Bernard Stefani. Characterizing contextual equivalence in calculi with passivation. Information and Computation, 209(11):1390-1433, 2011. Google Scholar
  12. 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. Google Scholar
  13. Adrien Piérard and Eijiro Sumii. A higher-order distributed calculus with name creation. In LICS'12, pages 531-540. IEEE, 2012. Google Scholar
  14. Davide Sangiorgi. Bisimulation for higher-order process calculi. Information and Computation, 131(2):141-178, 1996. Google Scholar
  15. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems, 33(1), 2011. Google Scholar
  16. Davide Sangiorgi and David Walker. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  17. 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. Google Scholar
  18. Bent Thomsen. Plain chocs: A second generation calculus for higher order processes. Acta Informatica, 30(1):1-59, 1993. Google Scholar