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