Paper: Eager Normal Form Bisimulation (at LICS 2005)
Authors: Soren LassenAbstract
This paper describes two new bisimulation equivalences for the pure untyped call-by-value ?-calculus, called enf bisimilarity and enf bisimilarity up to ?. They are based on eager reduction of terms to eager normal form (enf), analogously to co-inductive bisimulation characterizations of Lévy-Longo tree equivalence and Böhm tree equivalence (up to ?). We argue that enf bisimilarity is the call-by-value analogue of Lévy-Longo tree equivalence. Enf bisimilarity (up to ?) is the congruence on source terms induced by the call-by-value CPS transform and Böhm tree equivalence (up to ?) on target terms. Enf bisimilarity and enf bisimilarity up to ? enjoy powerful bisimulation proof principles which, among other things, can be used to establish a retraction theorem for the call-by-value CPS transform.
BibTeX
@InProceedings{Lassen-EagerNormalFormBisi, author = {Soren Lassen}, title = {Eager Normal Form Bisimulation}, booktitle = {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005}, year = 2005, editor = {Prakash Panangaden}, month = {June}, pages = {345--354}, location = {Chicago, USA}, publisher = {IEEE Computer Society Press} }