Specification and proof: Difference between revisions
No edit summary |
|||
| (One intermediate revision by one other user not shown) | |||
| 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 28: | 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 == | ||
| Line 34: | Line 37: | ||
* [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 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