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.

On the observational theory of the CPS-calculus (extended abstract)

MERRO, Massimo
;
2006-01-01

Abstract

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.
2006
CPS transforms
Operational semantics
Bisimulation-based techniques
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/29632
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact