Re: [isabelle] interpreters and continuations

Not in HOL (or other logics of total functions), but in the extension
HOLCF, which supports a separate type of continuous functions. I am not
sure if HOLCF has been used for this purpose before.


Jeremy Siek schrieb:
> 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?
> Cheers,
> Jeremy

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