We apply powerful proof-techniques of concurrency theory to study the observational theory of Thielecke’s CPS-calculus, a distillation of the target lan-guage of Continuation-Passing Style transforms. We define a labelled transition system 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 prop- erties on diverging terms that cannot be proved using the original axiomatic semantics of the CPS-calculus.
|Titolo:||On the observational theory of the CPS-calculus (extended abstract)|
MERRO, Massimo (Corresponding)
|Data di pubblicazione:||2006|
|Appare nelle tipologie:||04.01 Contributo in atti di convegno|