Difference between revisions of "Specification and proof"

From HaskellWiki
Jump to: navigation, search
 
(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

  • Sparkle is a theorem prover for the functional programming language Clean


E-mail, blog articles