Specification and proof

From HaskellWiki

This article is a stub. You can help by expanding it.

Contents 1 Introduction 2 In the real world 3 Papers 4 Software 5 E-mail, blog articles

1 Introduction

To do

2 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

3 Papers

• Research papers/Testing and correctness

4 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

5 E-mail, blog articles

• The thread "Specification and prover for Haskell" on the Haskell mailing list

• Djinn, Coq, Monad and a bit of Haskell

Categories: Stub articles | Development tools