On the Observational Theory of the CPS-calculus

We study the observational theory of Thielecke's (recursive) CPS-calculus, a target language for CPS transforms designed to bring out the jumping, imperative nature of continuation-passing. We define a labelled transition system for the CPS-calculus from which we derive a (weak) labelled bisimilarity that completely characterises Morris' context-equivalence. We prove a context lemma showing that Morris' context-equivalence coincides with a simpler context-equivalence closed under a certain class of contexts. Then we profit of the determinism of the CPS-calculus to give a simpler labelled characterisation of Morris' equivalence, resembling Abramsky's applicative bisimilarity. We enhance our bisimulation proof-methods with up-to bisimilarity and up-to context proof techniques. We use our bisimulation proof techniques to study the algebraic theory of the CPS-calculus proving two new algebraic laws that we conjecture cannot be derived using the original axiomatic semantics for the CPS-calculus. Finally, we prove the full abstraction of Thielecke's encoding of the CPS-calculus into a fragment of Fournet and Gonthier's Join-calculus with single pattern definitions.