Specification and proof
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
This article is a stub. You can help by expanding it.
Introduction
To do
In the real world
The Australian ICT research center Nicta has developed a verified micro kernel, see the following papers:
Papers
Software
- Applications and libraries/Theorem provers, tools for formal reasoning, written in Haskell
- The Programatica Project has an expressive logic called P-logic, and tools supporting it
- Sparkle is a theorem prover for the functional programming language Clean
- hs-to-coq converts Haskell into Coq
E-mail, blog articles
- The thread "Specification and prover for Haskell" on the Haskell mailing list