Email Gateway (Aug 18 2022 at 13:24): Email Gateway (Aug 18 2022 at 13:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Since Haskell is a pure language, reasoning about equational semantics
of Haskell programs is conceptually simple. To facilitate machine-aided
verification of Haskell programs further, we have developed a converter
from Haskell source files to Isabelle theory files: Haskabelle.
Both Haskabelle and Isabelle in combination allow to formally reason
about Haskell programs, particularly verifying partial correctness.
The conversion employed by Haskabelle covers only a subset of Haskell,
mainly since the higher-order logic of Isabelle has a more restrictive
type system than Haskell. A simple adaption mechanisms allows to tailor
the conversion process to specific needs.
So far, Haskabelle is working, but there is little experience for its
application in practice. Suggestions and feedback welcome.
See further
http://isabelle.in.tum.de/haskabelle.html
Florian
signature.asc
Last updated: May 03 2024 at 08:18 UTC