The Community for Technology Leaders
RSS Icon
Subscribe
Chicago, IL, USA
June 26, 2005 to June 29, 2005
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", LICS, 2005, Proceedings. 20th Annual IEEE Symposium on Logic in Computer Science, Proceedings. 20th Annual IEEE Symposium on Logic in Computer Science 2005, pp. 345-354, doi:10.1109/LICS.2005.15
17 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool