A Modular Structural Operational Semantics for Delimited Continuations
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.