On the observational theory of the CPS-calculus

We study the observational theory of Thielecke's CPS-calculus, a distillation of the target language of Continuation-Passing Style transforms. 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 smaller class of contexts. Then we profit of the determinism of the CPS-calculus to give a simpler labelled characterisation of Morris' equivalence, in the style of 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 investigate a few algebraic properties on diverging terms that cannot be proved using the original axiomatic semantics of the CPS-calculus. Finally, we prove the full abstraction of Thie...

• Type: Journal
• Year: 2010
• Where: ACTA
• Authors: Massimo Merro
• Keywords: ACTA 2010, Labelled Transition, Simpler Labelled Characterisation, Up-to Context Proof