Environmental bisimulations for higher-order languages

Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

Research output: Chapter in Book/Report/Conference proceedingConference contribution

55 Citations (Scopus)

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 λ-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 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 bisim-ulations, 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.

Original languageEnglish
Title of host publicationProceedings - 22nd Annual IEEE Symposiumon Logic in Computer Science, LICS 2007
Pages293-302
Number of pages10
DOIs
Publication statusPublished - 2007 Dec 1
Event22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007 - Wroclaw, Poland
Duration: 2007 Jul 102007 Jul 14

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Other

Other22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007
CountryPoland
CityWroclaw
Period07/7/1007/7/14

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Fingerprint Dive into the research topics of 'Environmental bisimulations for higher-order languages'. Together they form a unique fingerprint.

  • Cite this

    Sangiorgi, D., Kobayashi, N., & Sumii, E. (2007). Environmental bisimulations for higher-order languages. In Proceedings - 22nd Annual IEEE Symposiumon Logic in Computer Science, LICS 2007 (pp. 293-302). [4276573] (Proceedings - Symposium on Logic in Computer Science). https://doi.org/10.1109/LICS.2007.17