By Neil Sculthorpe, Paolo Torrini, and Peter D. Mosses
Abstract:
It has been an open question as to whether the Modular Structural Operational Semantics framework can express the dynamic semantics of call/cc. This paper shows that it can, and furthermore, demonstrates that it can express the more general delimited control operators control and shift.
In post-proceedings of the 2015 Workshop on Continuations, pages 63–80. Volume 212 of Electronic Proceedings in Theoretical Computer Science. Open Publishing Association, 2016.
Accompanying material
The archive includes:
- a suite of 70 test programs, written in (extended) Caml Light;
- a translation from Caml Light to funcons, together with the generated funcon programs;
- I-MSOS specifications of funcons and auxiliary entities, together with the Prolog code generated from them; and
- the tools for translation, generation and interpretation.