Specification and proof: Difference between revisions
No edit summary |
(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