# Difference between revisions of "Specification and proof"

From HaskellWiki

(Added Category:Development tools) |
(→Software) |
||

Line 30: | Line 30: | ||

* [http://www.cs.ru.nl/Sparkle/ Sparkle] is a theorem prover for the functional programming language Clean |
* [http://www.cs.ru.nl/Sparkle/ Sparkle] is a theorem prover for the functional programming language Clean |
||

+ | * [https://github.com/antalsz/hs-to-coq hs-to-coq] converts Haskell into Coq |
||

== E-mail, blog articles == |
== E-mail, blog articles == |

## Latest revision as of 01:58, 24 March 2018

*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