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

Taichi Yachi, Eijiro Sumii

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationProgramming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings
EditorsAtsushi Igarashi
PublisherSpringer Verlag
Pages171-186
Number of pages16
ISBN (Print)9783319479576
DOIs
Publication statusPublished - 2016
Event14th Asian Symposium on Programming Languages and Systems, APLAS 2016 - Hanoi, Viet Nam
Duration: 2016 Nov 212016 Nov 23

Publication series

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

Other

Other14th Asian Symposium on Programming Languages and Systems, APLAS 2016
Country/TerritoryViet Nam
CityHanoi
Period16/11/2116/11/23

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A sound and complete bisimulation for contextual equivalence in λ-calculus with call/cc'. Together they form a unique fingerprint.

Cite this