Difference between revisions of "Specification and proof"

From HaskellWiki
Jump to: navigation, search
(Added Category:Development tools)
(Software)
 
Line 30: 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 ==

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

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

E-mail, blog articles