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
ABSTRACT
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.
INDEX TERMS
null
CITATION
Soren Lassen, "Eager Normal Form Bisimulation", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 345-354, 2005, doi:10.1109/LICS.2005.15
86 ms
(Ver 3.3 (11022016))