Re: [isabelle] interpreters and continuations



Good to hear.

Does the code generation support work for HOLCF fixrec
definitions?

Cheers,
Jeremy

On Wed, Mar 4, 2009 at 9:22 AM, Brian Huffman <brianh at cs.pdx.edu> wrote:
> 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.
>
> - Brian
>
>
> 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.
>>
>> Tobias
>>
>> 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
>>>
>>
>>
>>
>
>
>
>
>



-- 
____________________________________
Jeremy Siek <jeremy.siek at colorado.edu>
http://ecee.colorado.edu/~siek/
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.