TY - GEN
T1 - A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc
AU - Yachi, Taichi
AU - Sumii, Eijiro
PY - 2016
Y1 - 2016
N2 - We develop a sound and complete proof method of contextual equivalence in λ-calculus with the abortive control operator call/cc (as opposed to delimited control operators like shift and reset), and prove the non-trivial equivalence between λf. f() and λf. f(); f() for example, both for the first time to our knowledge. Although our method is based on environmental bisimulations (Sumii et al. 2004-), it makes an essential and general change to their metatheory, which is not only necessary for handling call/cc but is also applicable in other languages with no control operator.
AB - We develop a sound and complete proof method of contextual equivalence in λ-calculus with the abortive control operator call/cc (as opposed to delimited control operators like shift and reset), and prove the non-trivial equivalence between λf. f() and λf. f(); f() for example, both for the first time to our knowledge. Although our method is based on environmental bisimulations (Sumii et al. 2004-), it makes an essential and general change to their metatheory, which is not only necessary for handling call/cc but is also applicable in other languages with no control operator.
UR - http://www.scopus.com/inward/record.url?scp=84992468369&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84992468369&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-47958-3_10
DO - 10.1007/978-3-319-47958-3_10
M3 - Conference contribution
AN - SCOPUS:84992468369
SN - 9783319479576
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 171
EP - 186
BT - Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings
A2 - Igarashi, Atsushi
PB - Springer Verlag
T2 - 14th Asian Symposium on Programming Languages and Systems, APLAS 2016
Y2 - 21 November 2016 through 23 November 2016
ER -