TY - GEN
T1 - A complete characterization of observational equivalence in polymorphic λ-calculus with general references
AU - Sumii, Eijiro
PY - 2009
Y1 - 2009
N2 - We give the first sound and complete proof method for observational equivalence in full polymorphic λ-calculus with existential types and first-class, higher-order references. Our method is syntactic and elementary in the sense that it only employs simple structures such as relations on terms. It is nevertheless powerful enough to prove many interesting equivalences that can and cannot be proved by previous approaches, including the latest work by Ahmed, Dreyer and Rossberg (POPL 2009).
AB - We give the first sound and complete proof method for observational equivalence in full polymorphic λ-calculus with existential types and first-class, higher-order references. Our method is syntactic and elementary in the sense that it only employs simple structures such as relations on terms. It is nevertheless powerful enough to prove many interesting equivalences that can and cannot be proved by previous approaches, including the latest work by Ahmed, Dreyer and Rossberg (POPL 2009).
UR - http://www.scopus.com/inward/record.url?scp=70350365548&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70350365548&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-04027-6_33
DO - 10.1007/978-3-642-04027-6_33
M3 - Conference contribution
AN - SCOPUS:70350365548
SN - 3642040268
SN - 9783642040269
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 455
EP - 469
BT - Computer Science Logic - 23rd International Workshop, CSL 2009 - 18th Annual Conference of the EACSL, Proceedings
T2 - 23rd International Workshop on Computer Science Logic, CSL 2009 - 18th Annual Conference of the EACSL
Y2 - 7 September 2009 through 11 September 2009
ER -