Re: [isabelle] interpreters and continuations
Certainly, using the HOLCF continuous function type should allow you
to define datatypes with continuations, just like you would define
them in Haskell or ML. The domain package currently allows you to use
indirect recursion with the continuous function space; for example,
you can declare types like this:
domain 'a foo = Foo "(foo -> 'a) -> 'a" | Bar 'a
Currently, support for indirect recursion is rather limited (you can't
use indirect recursion with arbitrary type constructors, due to
soundness concerns), and the domain package doesn't give you a very
useful induction rule for such types. But I am working on some big
improvements; the support for indirect recursion should get much
better within the next few months.
Quoting Tobias Nipkow <nipkow at in.tum.de>:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and