|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
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
| ASCII Text | x | ||
| Soren Lassen, "Eager Normal Form Bisimulation," Logic in Computer Science, Symposium on, pp. 345-354, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2005. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2005.15, author = {Soren Lassen}, title = {Eager Normal Form Bisimulation}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2005}, issn = {1043-6871}, pages = {345-354}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2005.15}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - Eager Normal Form Bisimulation SN - 1043-6871 SP345 EP354 A1 - Soren Lassen, PY - 2005 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
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.
