[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
http://isabelle.in.tum.de/haskabelle.html

	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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