Logic in Computer Science, Symposium on (2005)
June 26, 2005 to June 29, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2005.15
Soren Lassen , Google, Inc
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.
S. Lassen, "Eager Normal Form Bisimulation," 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05)(LICS), Chicago, IL, USA, 2005, pp. 345-354.