Environmental Bisimulations for Higher-Order Languages

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 environmental 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-byvalue), call-by-value λ-calculus with higher-order store, and then Higher-Order π-calculus. In each case: we present the basic properties of environmental 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 r...

• Type: Conference
• Year: 2007
• Where: LICS
• Authors: Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
• Keywords: Bisimulation, Bisimulation Proof Method, Computer Science, LICS 2007, Up-to Context