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.