Contextual equivalence for higher-order pi-calculus revisited

Alan Jeffrey; Julian Rathke

doi:10.2168/LMCS-1(1:4)2005

Alan Jeffrey ; Julian Rathke - Contextual equivalence for higher-order pi-calculus revisited

lmcs:2274 - Logical Methods in Computer Science, April 21, 2005, Volume 1, Issue 1 - https://doi.org/10.2168/LMCS-1(1:4)2005

Contextual equivalence for higher-order pi-calculus revisitedArticle

Authors: Alan Jeffrey ; Julian Rathke

The higher-order pi-calculus is an extension of the pi-calculus to allow communication of abstractions of processes rather than names alone. It has been studied intensively by Sangiorgi in his thesis where a characterisation of a contextual equivalence for higher-order pi-calculus is provided using labelled transition systems and normal bisimulations. Unfortunately the proof technique used there requires a restriction of the language to only allow finite types.
We revisit this calculus and offer an alternative presentation of the labelled transition system and a novel proof technique which allows us to provide a fully abstract characterisation of contextual equivalence using labelled transitions and bisimulations for higher-order pi-calculus with recursive types also.

https://doi.org/10.2168/LMCS-1(1:4)2005

Source: arXiv.org:cs/0503067

Volume: Volume 1, Issue 1

Published on: April 21, 2005

Imported on: September 17, 2004

Keywords: Computer Science - Programming Languages

Licence: arXiv.org - Assumed non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Collaborative Research: Temporal Aspects; Funder: National Science Foundation; Code: 0430175

Classifications

Mathematics Subject Classification 2020¹

68Q85 - Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Sources:

[1] zbMATH Open.

Bibliographic References

32 Documents citing this article

Dimitrios Kouzapas;Jorge A. Pérez;Nobuko Yoshida, 2016, Characteristic bisimulation for higher-order session processes, Acta Informatica, 54, 3, pp. 271-341, 10.1007/s00236-016-0289-7, https://doi.org/10.1007/s00236-016-0289-7.

Qiang Yin;Xian Xu;Huan Long, 2016, On parameterization of higher-order processes, International Journal of Computer Mathematics, 94, 7, pp. 1451-1478, 10.1080/00207160.2016.1210793.

Petar Maksimović;Alan Schmitt, 2015, HOCore in Coq, pp. 278-293, 10.1007/978-3-319-22102-1_19, https://hal.science/hal-01243017.

Mads Dam;Karl Palmskog, 2014, Location-independent routing in process network overlays, Service Oriented Computing and Applications, 9, 3-4, pp. 285-309, 10.1007/s11761-014-0173-7.

Mads Dam;Karl Palmskog, 2014, Location Independent Routing in Process Network Overlays, 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, 131, pp. 715-724, 10.1109/pdp.2014.30.

Xian Xu;Huan Long, 2014, A logical characterization for linear higher-order processes, Journal of Shanghai Jiaotong University (Science), 20, 2, pp. 185-194, 10.1007/s12204-014-1554-y.

Yuxin Deng, 2014, Weak Probabilistic Bisimulation, Semantics of Probabilistic Processes, pp. 233-245, 10.1007/978-3-662-45198-4_7.

Zining Cao, 2014, Normal Bisimulation for Higher Order Pi-Calculus with Unguarded Choice, 2014 Theoretical Aspects of Software Engineering Conference, 92, pp. 213-220, 10.1109/tase.2014.15.

JOACHIM PARROW;JOHANNES BORGSTRÖM;PALLE RAABJERG;JOHANNES ÅMAN POHJOLA, 2013, Higher-order psi-calculi, KTH Publication Database DiVA (KTH Royal Institute of Technology), 24, 2, 10.1017/s0960129513000170, http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-183610.

Vasileios Koutavas;Matthew Hennessy, 2013, Symbolic Bisimulation for a Higher-Order Distributed Language with Passivation, Lecture notes in computer science, pp. 167-181, 10.1007/978-3-642-40184-8_13.

Xian Xu, 2013, On Context Bisimulation for Parameterized Higher-order Processes, Electronic Proceedings in Theoretical Computer Science, 131, pp. 37-51, 10.4204/eptcs.131.5, https://doi.org/10.4204/eptcs.131.5.

Zining Cao, 2013, Normal Bisimulation for Higher Order Pi-Calculus with Unguarded Choice, 2013 International Symposium on Theoretical Aspects of Software Engineering, 3921, pp. 217-224, 10.1109/tase.2013.36.

Yuxin Deng;Matthew Hennessy, 2012, On the semantics of Markov automata, Information and Computation, 222, pp. 139-168, 10.1016/j.ic.2012.10.010.

Yuxin Deng;Yuan Feng, 2012, Open Bisimulation for Quantum Processes, Lecture notes in computer science, pp. 119-133, 10.1007/978-3-642-33475-7_9, https://doi.org/10.1007/978-3-642-33475-7_9.

Zining Cao, 2012, More on bisimulations for higher order π-calculus, Theoretical Computer Science, 446, pp. 1-19, 10.1016/j.tcs.2012.04.014.

Andrew Pitts, 2011, Howe's method for higher-order languages, Cambridge University Press eBooks, pp. 197-232, 10.1017/cbo9780511792588.006.

Davide Sangiorgi;Naoki Kobayashi;Eijiro Sumii, 2011, Environmental bisimulations for higher-order languages, ACM Transactions on Programming Languages and Systems, 33, 1, pp. 1-69, 10.1145/1889997.1890002, https://doi.org/10.1145/1889997.1890002.

Ross Horne;Vladimiro Sassone, 2011, A Verified Algebra for Linked Data, Electronic Proceedings in Theoretical Computer Science, 58, pp. 20-33, 10.4204/eptcs.58.2, https://doi.org/10.4204/eptcs.58.2.

Sergueï Lenglet;Alan Schmitt;Jean-Bernard Stefani, 2011, Characterizing contextual equivalence in calculi with passivation, Information and Computation, 209, 11, pp. 1390-1433, 10.1016/j.ic.2011.08.002.

Vasileios Koutavas;Matthew Hennessy, 2011, A Testing Theory for a Higher-Order Cryptographic Language, Lecture notes in computer science, pp. 358-377, 10.1007/978-3-642-19718-5_19, https://doi.org/10.1007/978-3-642-19718-5_19.

Yuxin Deng;Matthew Hennessy, 2011, On the Semantics of Markov Automata, Lecture notes in computer science, pp. 307-318, 10.1007/978-3-642-22012-8_24.

Fabrizio Montesi;Davide Sangiorgi, 2010, A Model of Evolvable Components, Lecture notes in computer science, pp. 153-171, 10.1007/978-3-642-15640-3_11.

Ivan Lanese;Jorge A. Pérez;Davide Sangiorgi;Alan Schmitt, 2010, On the expressiveness and decidability of higher-order process calculi, SPIRE - Sciences Po Institutional REpository, 209, 2, pp. 198-226, 10.1016/j.ic.2010.10.001, https://inria.hal.science/hal-01112294.

Sergueï Lenglet;Alan Schmitt;Jean-Bernard Stefani, 2009, Howe’s Method for Calculi with Passivation, Lecture notes in computer science, pp. 448-462, 10.1007/978-3-642-04081-8_30.

Zining Cao, 2009, Branching Bisimulations for Higher Order p-Calculus, 2009 International Conference on Information Technology and Computer Science, 60, pp. 522-525, 10.1109/itcs.2009.275.

Ivan Lanese;Jorge A. Perez;Davide Sangiorgi;Alan Schmitt, 2008, On the Expressiveness and Decidability of Higher-Order Process Calculi, SPIRE - Sciences Po Institutional REpository, 3921, pp. 145-155, 10.1109/lics.2008.8, https://inria.hal.science/inria-00494584.

Julian Rathke;Paweł Sobociński, 2008, Deconstructing behavioural theories of mobility, IFIP International Federation for Information Processing/IFIP, pp. 507-520, 10.1007/978-0-387-09680-3_34, https://doi.org/10.1007/978-0-387-09680-3_34.

Davide Sangiorgi;Naoki Kobayashi;Eijiro Sumii, 2007, Environmental Bisimulations for Higher-Order Languages, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp. 293-302, 10.1109/lics.2007.17.

J. Laird, 2006, Game Semantics for Higher-Order Concurrency, Lecture notes in computer science, pp. 417-428, 10.1007/11944836_38.

M.A. Ghafoor;Jianwei Yin;Jinxiang Dong;M. Mujeeb-u-Rehman, 2005, Service-oriented Mobile Calculus Technology in M-Business interoperability between Customer and e-Shop, IEEE International Workshop on Service-Oriented System Engineering (SOSE'05), 30, pp. 191-198, 10.1109/sose.2005.33.

Massimo Merro;Francesco Zappa Nardelli, 2005, Behavioral theory for mobile ambients, Journal of the ACM, 52, 6, pp. 961-1023, 10.1145/1101821.1101825.

D. Sangiorgi, 2004, Bisimulation: from the origins to today, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., 62, pp. 298-302, 10.1109/lics.2004.1319624.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3146 times.

This article's PDF has been downloaded 521 times.