[isabelle] interpreters and continuations

Lately I've been investigating writing interpreters in Isabelle/HOL and
ran into a problem when trying to support first-class continuations. The
typical approach when writing an interpreter in ML or Haskell is to
write the interpreter in continuation passing style (or monadic style)
and to embed the continuations as functions in the value (or expression)
datatype. Of course, in Isabelle/HOL this is not possible.

Using alternative approaches, such as SOS or abstract machines, this is not
a problem because continuations are represented explicitly as data.

At this point I'm thinking that one can't write an interpreter in Isabelle
that supports first-class continuations, but perhaps I'm overlooking something?


Jeremy Siek <jeremy.siek at colorado.edu>
Assistant Professor
Dept. of Electrical, Computer, and Energy Engineering
University of Colorado at Boulder

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.