[isabelle] Announcing Haskabelle2009

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




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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