20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05) Eager Normal Form Bisimulation Chicago, Illinois June 26-June 29 ISBN: 0-7695-2266-1
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2005.15
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.
Citation:
Soren Lassen, "Eager Normal Form Bisimulation," lics, pp.345-354, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2005 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||