Specification and proof

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:

• Pre/post verification and refinement of state monad programs

• Experience report on the Haskell verification

• seL4: Formal Verification of an OS Kernel

• A list of best publications in the L4.verified project

Papers

• Research papers/Testing and correctness

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

• Djinn, Coq, Monad and a bit of Haskell