Difference between revisions of "Specification and proof"
Jump to navigation
Jump to 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
- 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