@INPROCEEDINGS{SKS07,
  title = {{Environmental Bisimulations for Higher-Order Languages}},
  author = {{Davide} {Sangiorgi} and {Naoki} {Kobayashi} and {Eijiro} {Sumii}},
  booktitle = {Proc. of LICS 2007},
  pages = {293-302},
  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 environmental bisimulations, a form of bisimulation for higher-order languages, and its basic theory. We consider four representative calculi: pure lambda-calculi (call-by-name and call-by-value), call-by-value lambda-calculus with higher-order store, and then Higher-Order pi-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 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 lambda-calculi to the richer calculi with simple congruence proofs.},
  publisher = {IEEE Computer Society},
  year = {2007},
  url = {http://www.cs.unibo.it/~sangio/DOC_public/env.pdf},
  address = {Wroclaw, Poland},
  doi = {10.1109/LICS.2007.17},
  invited = {N},
  partner = {UNIBO},
  status = {public},
  task = {T3.4},
}