Hello,

In an attempt to wrap my head around this SRFI I've written down a CPS
abstract machine semantics for the control operators in the Dybvig
paper, modified with continuation marks and abstracted to handle
multiple value functions.

The semantics have a few metafunctions that don't have formal
definitions because I wanted to focus on embedding marks and delimited
control operators. As such, it's more of a sketch.

The eventual goal is to write an interpreter for a Scheme with the
operations in this SRFI. A good semantics would help me write optimized
versions of some procedures that are expressible in the Dybvig paper
(like call-with-non-composable-continuation).

Here is a link to it:

https://florida.moe/r7rs/delimited-continuations/model.xhtml

Comments welcome. (I have no background in formal mathematics or
computer science, and this is the first time I've tried writing
something like this.)

-- Peter McGoron