A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc

Taichi Yachi; Eijiro Sumii

doi:10.1007/978-3-319-47958-3_10

A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc

Taichi Yachi, Eijiro Sumii

INF - Computer and Mathematical Sciences

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings
Editors	Atsushi Igarashi
Publisher	Springer Verlag
Pages	171-186
Number of pages	16
ISBN (Print)	9783319479576
DOIs	https://doi.org/10.1007/978-3-319-47958-3_10
Publication status	Published - 2016
Event	14th Asian Symposium on Programming Languages and Systems, APLAS 2016 - Hanoi, Viet Nam Duration: 2016 Nov 21 → 2016 Nov 23

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10017 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	14th Asian Symposium on Programming Languages and Systems, APLAS 2016
Country/Territory	Viet Nam
City	Hanoi
Period	16/11/21 → 16/11/23

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-47958-3_10

Cite this

Yachi, T., & Sumii, E. (2016). A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc. In A. Igarashi (Ed.), Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings (pp. 171-186). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10017 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-47958-3_10

A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc. / Yachi, Taichi; Sumii, Eijiro.

Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings. ed. / Atsushi Igarashi. Springer Verlag, 2016. p. 171-186 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10017 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Yachi, T & Sumii, E 2016, A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc. in A Igarashi (ed.), Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10017 LNCS, Springer Verlag, pp. 171-186, 14th Asian Symposium on Programming Languages and Systems, APLAS 2016, Hanoi, Viet Nam, 16/11/21. https://doi.org/10.1007/978-3-319-47958-3_10

Yachi T, Sumii E. A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc. In Igarashi A, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings. Springer Verlag. 2016. p. 171-186. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-47958-3_10

Yachi, Taichi ; Sumii, Eijiro. / A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc. Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings. editor / Atsushi Igarashi. Springer Verlag, 2016. pp. 171-186 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{882f8fc4f9724eb28e31f9285b71ac0b,

title = "A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc",

abstract = "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.",

author = "Taichi Yachi and Eijiro Sumii",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 14th Asian Symposium on Programming Languages and Systems, APLAS 2016 ; Conference date: 21-11-2016 Through 23-11-2016",

year = "2016",

doi = "10.1007/978-3-319-47958-3_10",

language = "English",

isbn = "9783319479576",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "171--186",

editor = "Atsushi Igarashi",

booktitle = "Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings",

}

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 -

A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this