From higher-order logic to Haskell: there and back again

We present two tools which together allow reasoning about (a substantial subset of) Haskell programs. One is the code generator of the proof assistant Isabelle, which turns specifications formulated in Isabelle’s higher-order logic into executable Haskell source text; the other is Haskabelle, a tool to translate programs written in Haskell into Isabelle specifications. The translation from Isabelle to Haskell directly benefits from the rigorous correctness approach of a proof assistant: generated Haskell programs are always partially correct w.r.t. to the specification from which they are generated.

• Type: Conference
• Year: 2010
• Where: PEPM
• Authors: Florian Haftmann
• Keywords: Executable Haskell Source, Haskell Programs, PEPM 2010, Proof Assistant Isabelle, Software Engineering