Personal tools

Specification and proof

From HaskellWiki

(Difference between revisions)
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]]

Latest revision as of 13:16, 25 May 2013

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

Contents

[edit] 1 Introduction

To do


[edit] 2 In the real world

The Australian ICT research center Nicta has developed a verified micro kernel, see the following papers:


[edit] 3 Papers


[edit] 4 Software

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


[edit] 5 E-mail, blog articles