Davide Sangiorgi
Eijiro Sumii
Abstract
Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, as well as enhancements of the bisimulation proof method with “up-to context” techniques, and (2) obtaining definitions and results that scale to languages with different features.
To meet these challenges, we present environment{} bisimulations, a form of bisimulation for higher-order languages, and its basic theory. We consider four representative calculi: pure λ-calculi (call-by-name and call-by-value), call-by-value λ-calculus with higher-order store, and then Higher-Order π-calculus. In each case: we present the basic properties of environment bisimilarity, including congruence; we show that it coincides with contextual equivalence; we develop some up-to techniques, including up-to context, as examples of possible enhancements of the associated bisimulation method.
Unlike previous approaches (such as applicative bisimulations, logical relations, Sumii-Pierce-Koutavas-Wand), our method does not require induction/indices on evaluation derivation/steps (which may complicate the proofs of congruence, transitivity, and the combination with up-to techniques), or sophisticated methods such as Howe's for proving congruence. It also scales from the pure λ-calculi to the richer calculi with simple congruence proofs.
- Abadi, M. and Gordon, A. D. 1998. A bisimulation method for cryptographic protocols. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 1381. Springer, 12--26. Google Scholar
Digital Library
- Abramsky, S. 1990. The lazy lambda calculus. In Research Topics in Functional Programming, D. A. Turner, Ed., Addison-Wesley, 65--117. Google ScholarDigital Library
- Ahmed, A. 2006. Step-indexed syntactic logical relations for recursive and quantified types. In Proceedings of the European Symposium on Programming (ESOP). 69--83. Google ScholarDigital Library
- Ahmed, A., Appel, A. W., and Virga, R. 2003. An indexed model of impredicative polymorphism and mutable references. http://www.cs.princeton.edu/~amal/papers/impred.pdf.Google Scholar
- Ahmed, A., Dreyer, D., and Rossberg, A. 2009. State-dependent representation independence. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). 340--353. Google ScholarDigital Library
- Appel, A. W. and McAllester, D. 2001. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23, 5, 657--683. Google ScholarDigital Library
- Baldamus, M. and Frauenstein, T. 1995. Congruence proofs for weak bisimulation equivalences on higher--order process calculi. Report 95--21, Computer Science Department, Berlin University of Technology.Google Scholar
- Birkedal, L. and Harper, R. 1999. Relational interpretations of recursive types in an operational setting. Inform. Comput. 155, 1--2, 3--63. Google ScholarDigital Library
- Boreale, M., De Nicola, R., and Pugliese, R. 1999. Proof techniques for cryptographic processes. In Proceedings of the Annual IEEE Symposium on Login in Computer Science (LICS). IEEE, Computer Society Press, 157--166. Google ScholarDigital Library
- Boreale, M. and Sangiorgi, D. 1998. Bisimulation in name-passing calculi without matching. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press. Google ScholarDigital Library
- Cao, Z. 2006. More on bisimulations for higher order pi-calculus. In Proc. FoSSaCS'06. Lecture Notes in Computer Science, vol. 3921. Springer, 63--78. Google ScholarDigital Library
- Crary, K. and Harper, R. 2000. Syntactic logical relations over polymorphic and recursive types. Draft.Google Scholar
- Ferreira, W., Hennessy, M., and Jeffrey, A. 1998. A theory of weak bisimulation for core CML. J. Func. Program. 8, 5, 447--491. Google ScholarDigital Library
- Godskesen, J. and Hildebrandt, T. 2005. Extending Howe's method to early bisimulations for typed mobile embedded resources with local names. In Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). Lecture Notes in Computer Science, vol. 3821. Springer, 140--151. Google ScholarDigital Library
- Gordon, A. D. 1993. Functional programming and input/output. Ph.D. thesis, University of Cambridge.Google Scholar
- Honda, K. and Yoshida, N. 1995. On reduction-based process semantics. Theor. Comput. Sci. 152, 2, 437--486. Google ScholarDigital Library
- Howe, D. J. 1996. Proving congruence of bisimulation in functional programming languages. Info. Comput. 124, 2, 103--112. Google ScholarDigital Library
- Jeffrey, A. and Rathke, J. 1999. Towards a theory of bisimulation for local names. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS). 56--66. Google ScholarDigital Library
- Jeffrey, A. and Rathke, J. 2004. A theory of bisimulation for a fragment of concurrent ml with local names. Theor. Comput. Sci. 323, 1-3, 1--48. Google ScholarDigital Library
- Jeffrey, A. and Rathke, J. 2005. Contextual equivalence for higher-order pi-calculus revisited. Logic. Meth. Comput. Sci. 1, 1:4, 1--22.Google Scholar
- Koutavas, V. and Wand, M. 2006a. Bisimulations for untyped imperative objects. In Proceedings of the European Symposium on Programming (ESOP). 146--161. Google ScholarDigital Library
- Koutavas, V. and Wand, M. 2006b. Small bisimulations for reasoning about higher-order imperative programs. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). 141--152. Google ScholarDigital Library
- Lassen, S. B. 1998. Relational reasoning about functions and nondeterminism. Ph.D. thesis, Department of Computer Science, University of Aarhus.Google Scholar
- Lenglet, S. 2010. Bisimulations dans les calculs avec passivation. Ph.D. thesis, Université Joseph Fourier, Grenoble.Google Scholar
- Lenglet, S., Schmitt, A., and Stefani, J.-B. 2009. Howe's method for calculi with passivation. In Proceedings of the International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 5710. 448--462. Google ScholarDigital Library
- Merro, M. and Hennessy, M. 2002. Bisimulation congruences in Safe Ambients. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). 71--80. Google ScholarDigital Library
- Merro, M. and Nardelli, F. Z. 2005. Behavioral theory for mobile ambients. J. ACM 52, 6, 961--1023. Google ScholarDigital Library
- Milner, R. 1989. Communication and Concurrency. Prentice Hall. Google ScholarDigital Library
- Milner, R. 1999. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press. Google ScholarDigital Library
- Milner, R. 2006. Pure bigraphs: Structure and dynamics. Inform. Comput. 204, 1, 60--122. Google ScholarDigital Library
- Mitchell, J. C. 1996. Foundations for Programming Languages. MIT Press. Google ScholarDigital Library
- Morris, J. H., Jr. 1968. Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology.Google Scholar
- Ong, L. 1988. The lazy lambda calculus: an investigation into the foundations of functional programming. Ph.D. thesis, University of London.Google Scholar
- Pierce, B. C. and Sangiorgi, D. 2000. Behavioral equivalence in the polymorphic pi-calculus. J. ACM 47, 3, 531--586. Google ScholarDigital Library
- Pitts, A. 1997. Operationally-based theories of program equivalence. In Semantics and Logics of Computation, A. M. Pitts and P. Dybjer Eds., Publications of the Newton Institute., Cambridge University Press, 241--298.Google Scholar
- Pitts, A. 2005. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, B. C. Pierce Ed., MIT Press, Chapter 7, 245--289.Google Scholar
- Pous, D. 2008. Techniques modulo pour les bisimulations. Ph.D. thesis, ENS Lyon.Google Scholar
- Pous, D. and Sangiorgi, D. Enhancements of the bisimulation proof method.Google Scholar
- Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. In Inf. Proceedings of the IFIP 9th World Computer Congres. 513--523.Google Scholar
- Sands, D. 1998. Improvement theory and its applications. In Higher Order Operational Techniques in Semantics, A. D. Gordon and A. M. Pitts Eds., Publications of the Newton Institute, Cambridge University Press, 275--306. Google ScholarDigital Library
- Sangiorgi, D. 1992. Expressing mobility in process algebras: First-order and higher-order paradigm. Ph.D. thesis, University of Edinburgh.Google Scholar
- Sangiorgi, D. 1994. The lazy lambda calculus in a concurrency scenario. Inform. Comput. 111, 1, 120--153. Google ScholarDigital Library
- Sangiorgi, D. 1996. Bisimulation for Higher-Order Process Calculi. Inform. Comput. 131, 2, 141--178. Google ScholarDigital Library
- Sangiorgi, D. 2001. Asynchronous process calculi: the first-order and higher-order paradigms (tutorial). Theor. Comput. Sci. 253, 311--350. Google ScholarDigital Library
- Sangiorgi, D., Kobayashi, N., and Sumii, E. 2007. Logical bisimulations and functional languages. In Proceedings of the international Symposium on Fundamentals of Software Engineering (FSEN). Lecture Notes in Computer Science, vol. 4767. Springer, 364--379. Google ScholarDigital Library
- Sangiorgi, D. and Walker, D. 2001. The π-calculus: a Theory of Mobile Processes. Cambridge University Press. Google ScholarDigital Library
- Schmitt, A. and Stefani, J.-B. 2004. The kell calculus: A family of higher-order distributed process calculi. In Proceedings of the International Conference on Global Computing. Lecture Notes in Computer Science, vol. 3267. Springer, 146--178. Google ScholarDigital Library
- Støvring, K. and Lassen, S. B. 2007. A complete, co-inductive syntactic theory of sequential control and state. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). 161--172. To appear. Google ScholarDigital Library
- Sumii, E. 2009. A complete characterization of observational equivalence in polymorphic λ-calculus with general references. In Proceedings of the International Conference on Computer Science Logic, Lecture Notes in Computer Science, vol. 5771, Springer-Verlag, 455--469. Google ScholarDigital Library
- Sumii, E. and Pierce, B. C. 2003. Logical relations for encryption. J. Comput. Secu. 11, 4, 521--554. Google ScholarDigital Library
- Sumii, E. and Pierce, B. C. 2007a. A bisimulation for dynamic sealing. Theor. Comput. Sci. 375, 1-3, 169--192. Google ScholarDigital Library
- Sumii, E. and Pierce, B. C. 2007b. A bisimulation for type abstraction and recursion. J. ACM 54, 5. Google ScholarDigital Library
- Thomsen, B. 1993. Plain CHOCS, a second generation calculus for higher-order processes. Acta Informatica 30, 1--59.Google ScholarDigital Library
Index Terms
- Environmental bisimulations for higher-order languages
Recommendations
Environmental Bisimulations for Higher-Order Languages
LICS '07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer ScienceDeveloping a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, as well as enhancements of the bisimulation proof method with "up-to context" techniques, and (2) obtaining ...
Environmental bisimulations for probabilistic higher-order languages
POPL '16Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the ...
Environmental bisimulations for probabilistic higher-order languages
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesEnvironmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the ...
Reviews
Prahladavaradan Sampath
Bisimulation has a long history as a technique for studying the equivalence of mathematical structures. A recurring theme in the literature of bisimulation is the characterization of semantic equivalence of expressions in a language. For example, an early result in bisimulation characterizes logical equivalence of formulae in modal logics [1]. Another well-known example is the characterization of observational equivalence of processes in the calculus of communicating systems (CCS) [2]. An appealing aspect of using bisimulation to study equivalence is its use of concrete operational notions such as reduction; this is in contrast to more abstract approaches followed by a denotational semantic approach to equivalence. This paper follows the tradition of using bisimulation to study equivalence of higher-order programming languages and process calculi. The literature has a rich theory of higher-order bisimulation, where bisimulation is defined as an equivalence relation over terms. Most of these approaches define bisimulation using some form of universal quantification over contexts in order to characterize contextual equivalence in higher-order languages. The primary contribution of this paper is to relativize the bisimulation relation with respect to an environment that encodes "knowledge" of the contexts to be considered. This formulation leads to more local reasoning with bisimulations. The paper also develops techniques for effectively reasoning with this enhanced bisimulation relation. The paper demonstrates the power of this approach by developing theories of bisimulation for a variety of higher-order languages. The current formulation of bisimulation using environments brings the study of bisimulation closer to denotational theories of equivalence. For example, there seems to be some similarity between the notion of history in game semantics [3] and the environment in environmental bisimulations. In some sense, this convergence is to be expected, given that both approaches study the same phenomena; however, such a full unification of the different approaches to equivalence still remains a goal to which to aspire. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments