Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
Environmental Bisimulations for Higher-Order Languages @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}, }
|