Abstract
The bisimulation proof method can be enhanced by employing ‘bisimulations up-to’ techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on the notion of compatible function for fixed-point theory.
We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the π-calculus, the λ-calculus, and a (call-by-value) λ-calculus with references.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 12–26. Springer, Heidelberg (1998)
Abramsky, S.: The lazy lambda calculus. In: Turner, D. (ed.) Research Topics in Functional Programming, pp. 65–116. Addison-Wesley (1989)
Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Informatica 29, 737–760 (1992)
Chaudhuri, K., Cimini, M., Miller, D.: Formalization of the bisimulation-up-to technique and its meta theory. Draft (2014)
Hirschkoff, D.: A full formalisation of pi-calculus theory in the calculus of constructions. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 153–169. Springer, Heidelberg (1997)
Hur, C.-K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: POPL, pp. 193–206. ACM (2013)
Jeffrey, A., Rathke, J.: Towards a theory of bisimulation for local names. In: LICS, pp. 56–66 (1999)
Koutavas, V., Hennessy, M.: First-order reasoning for higher-order concurrency. Computer Languages, Systems & Structures 38(3), 242–277 (2012)
Koutavas, V., Levy, P.B., Sumii, E.: From applicative to environmental bisimulation. Electr. Notes Theor. Comput. Sci. 276, 215–235 (2011)
Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: POPL 2006, pp. 141–152. ACM (2006)
Lassen, S.B.: Relational reasoning about contexts. In: Higher-order Operational Techniques in Semantics, pp. 91–135. Cambridge University Press (1998)
Lassen, S.B.: Relational Reasoning about Functions and Nondeterminism. PhD thesis, Department of Computer Science, University of Aarhus (1998)
Lassen, S.B.: Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. Electr. Notes Theor. Comput. Sci. 20, 346–374 (1999)
Lenisa, M.: Themes in Final Semantics. Ph.D. thesis, Universitá di Pisa (1998)
Madiot, J.-M., Pous, D., Sangiorgi, D.: Web appendix to this paper, http://hal.inria.fr/hal-00990859
Merro, M., Nardelli, F.Z.: Behavioral theory for mobile ambients. J. ACM 52(6), 961–1023 (2005)
Milner, R.: Communication and Concurrency. Prentice Hall (1989)
Pohjola, J.Å., Parrow, J.: Bisimulation up-to techniques for psi-calculi. Draft (2014)
Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: Advanced Topics in Bisimulation and Coinduction. Cambridge University Press (2012)
Rot, J., Bonsangue, M., Rutten, J.: Coalgebraic bisimulation-up-to. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol. 7741, pp. 369–381. Springer, Heidelberg (2013)
Sangiorgi, D.: On the bisimulation proof method. J. of MSCS 8, 447–479 (1998)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33(1), 5 (2011)
Sangiorgi, D., Walker, D.: The Pi-Calculus: a theory of mobile processes. Cambridge University Press (2001)
Sumii, E., Pierce, B.C.: A bisimulation for dynamic sealing. Theor. Comput. Sci. 375(1-3), 169–192 (2007)
Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. J. ACM 54(5) (2007)
Turner, N.D.: The polymorphic pi-calculus: Theory and Implementation. PhD thesis, Department of Computer Science, University of Edinburgh (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Madiot, JM., Pous, D., Sangiorgi, D. (2014). Bisimulations Up-to: Beyond First-Order Transition Systems. In: Baldan, P., Gorla, D. (eds) CONCUR 2014 – Concurrency Theory. CONCUR 2014. Lecture Notes in Computer Science, vol 8704. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44584-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-662-44584-6_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44583-9
Online ISBN: 978-3-662-44584-6
eBook Packages: Computer ScienceComputer Science (R0)