# Difference between revisions of "Specification and proof"

From HaskellWiki

(Added Category:Development tools) |
|||

Line 6: | Line 6: | ||

== In the real world == |
== In the real world == |
||

+ | |||

The Australian ICT research center [http://www.nicta.com.au/ Nicta] has developed a [http://www.ertos.nicta.com.au/research/l4.verified/ verified micro kernel], see the following papers: |
The Australian ICT research center [http://www.nicta.com.au/ Nicta] has developed a [http://www.ertos.nicta.com.au/research/l4.verified/ verified micro kernel], see the following papers: |
||

* [http://www.cse.unsw.edu.au/~kleing/papers/Cock_KS_08.html Pre/post verification and refinement of state monad programs] |
* [http://www.cse.unsw.edu.au/~kleing/papers/Cock_KS_08.html Pre/post verification and refinement of state monad programs] |
||

Line 22: | Line 23: | ||

== Software == |
== Software == |
||

+ | |||

* [[Applications and libraries/Theorem provers]], tools for formal reasoning, written in Haskell |
* [[Applications and libraries/Theorem provers]], tools for formal reasoning, written in Haskell |
||

Line 34: | Line 36: | ||

* [http://www.alpheccar.org/en/posts/show/70 Djinn, Coq, Monad and a bit of Haskell] |
* [http://www.alpheccar.org/en/posts/show/70 Djinn, Coq, Monad and a bit of Haskell] |
||

+ | |||

+ | |||

+ | |||

+ | [[Category:Development tools]] |

## Revision as of 13:16, 25 May 2013

*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

## E-mail, blog articles

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