Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Haskabelle

Email Gateway (Aug 22 2022 at 15:14):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Isabelle users,

up until Isabelle2016 there has been a neat tool called Haskabelle
(http://isabelle.in.tum.de/repos/haskabelle) allowing to import Haskell
source files into Isabelle/HOL theories (within certain bounds).

As it seems, this is no longer maintained.

My impression is that Haskabelle is maybe not used for big projects but
a neat tool for beginners to get acquainted with Isabelle/HOL.

How do Isabelle users see Haskabelle? That question is important since
there are considerable maintainance efforts required to make it usable
again within the contemporary biotope (somewhere around GHC 7.10.3 and
Isabelle2016-1).

Being curious for your responses,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 15:14):

From: Andrew Butterfield <Andrew.Butterfield@scss.tcd.ie>
Dear Florian and Isabelle Users,

we (Artur Gomes and myself) are currently using it on a project to very code written in Haskell

• we've had some correspondence over its status in which you were involved.

I'd be interested in getting it up-to-date again, but am not sure how time I could spare

• certainly I'd not be able to do much before July
• but I do have a long term interest in having Haskell and Isabelle play nice together...

Regards, Andrew

Andrew Butterfield
School of Computer Science & Statistics
Trinity College
Dublin 2, Ireland

Email Gateway (Aug 22 2022 at 15:14):

From: Lawrence Paulson <lp15@cam.ac.uk>
I have never used it myself, but a tool to assist in verifying Haskell programs seems potentially important.
Larry

Last updated: Apr 25 2024 at 12:23 UTC