Re: [isabelle] HOLCF

we have implemented a translation of Haskell into Isabelle HOLCF as part of the Heterogeneous Tool Set, see This has been done some years ago and probably would need to be adapted to the latest Isabelle version, though.

Best, Till

Am 27.06.2012 13:41, schrieb Tobias Nipkow:
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.


Prof. Dr. Till Mossakowski  Cartesium, room 2.51 Phone +49-421-218-64226
DFKI GmbH Bremen                             Fax +49-421-218-9864226
Cyber-Physical Systems                      Till.Mossakowski at
Enrique-Schmidt-Str. 5, D-28359 Bremen

Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
principal office, *not* the address for mail etc.!!!:
Trippstadter Str. 122, D-67663 Kaiserslautern
management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff
supervisory board: Prof. Hans A. Aukes (chair)
Amtsgericht Kaiserslautern, HRB 2313

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