The Community for Technology Leaders
Logic in Computer Science, Symposium on (2005)
Chicago, Illinois
June 26, 2005 to June 29, 2005
ISSN: 1043-6871
ISBN: 0-7695-2266-1
pp: 345-354
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.
87 ms
(Ver 3.3 (11022016))