Re: [isabelle] HOLCF

Am 27/06/2012 07:36, schrieb Christian Sternagel:
> Currently if we want to verify Haskell code, we have to take the sources,
> translate them (manually?) into Isabelle

There is Haskabelle for translating Haskelle to HOL. But data types become eager
in the process. One would need a similar translation to HOLCF.

Of course I agree that code generation for HOLCF would be very nice to have. We
had this on the agenda at some point - maybe we should get back to it.


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