[Haskell] Specification and prover for Haskell

Romain Demeyer

unread,

Oct 25, 2010, 4:09:48 AM10/25/10

to has...@haskell.org

Hello,

I'm working on static verification in Haskell, and I search for existing
works on specification of Haskell programs (such as pre/post conditions, for
example) or any other functional language. It would be great if there exists
a prover based on this kind of specifications. I already found the
ESC/Haskell. Do you know some other works which could be interesting?

Thanks,

rde.

Janis Voigtländer

unread,

Oct 25, 2010, 4:18:10 AM10/25/10

to Romain Demeyer, has...@haskell.org

Might be of interest: http://www.cs.ru.nl/Sparkle/

Romain Demeyer schrieb:

> ------------------------------------------------------------------------
>
> _______________________________________________
> Haskell mailing list
> Has...@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell

--
Jun.-Prof. Dr. Janis Voigtl�nder
http://www.iai.uni-bonn.de/~jv/
mailto:j...@iai.uni-bonn.de
_______________________________________________
Haskell mailing list
Has...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Jean-Marie Gaillourdet

unread,

Oct 25, 2010, 7:52:37 AM10/25/10

to Romain Demeyer, has...@haskell.org

Hi Romain,

are you aware of Haskabelle [1], a Haskell to Isabelle/HOL converter?
I've never used or investigated it.

-- Jean

[1] http://isabelle.in.tum.de/haskabelle.html

Dominique Devriese

unread,

Oct 25, 2010, 8:13:18 AM10/25/10

to Haskell-Cafe

Romain,

2010/10/25 Romain Demeyer <r...@info.fundp.ac.be>:

I found the paper "Verifying Haskell using constructive type theory"
[1] interesting...

Dominique

Footnotes:
[1] http://www.mimuw.edu.pl/~ben/Papers/monadic.pdf
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Tristan Allwood

unread,

Oct 25, 2010, 8:52:57 AM10/25/10

to has...@haskell.org, ws...@doc.ic.ac.uk, r...@info.fundp.ac.be

Hi,

You might also want to have a look at Zeno, being developed by Will
Sonnex (cc'd) which is in this space
http://www.doc.ic.ac.uk/~ws506/tryzeno/

Cheers,

Tris

> _______________________________________________

Gerwin Klein

unread,

Oct 25, 2010, 6:32:46 PM10/25/10

to Romain Demeyer, has...@haskell.org

On 25/10/2010, at 7:09 PM, Romain Demeyer wrote:
> I'm working on static verification in Haskell, and I search for existing works on specification of Haskell programs (such as pre/post conditions, for example) or any other functional language.

We have used Haskell extensively in the verification of the seL4 microkernel. One part of that was translating a prototype of the kernel into Isabelle and proving a large number of invariants as well as proving two refinement theorems about the translation. For our work the translation itself was not correctness critical, so we were happy to use our own somewhat ad-hoc tool for it.

Some papers on this are:

Pre/post verification and refinement of state monad programs:
http://www.cse.unsw.edu.au/~kleing/papers/Cock_KS_08.html

Experience report on the Haskell verification:
http://www.cse.unsw.edu.au/~kleing/papers/Klein_DE_09.html

The whole picture:
http://www.cse.unsw.edu.au/~kleing/papers/sosp09.html

More papers here:
http://www.ertos.nicta.com.au/research/l4.verified/pubs.pml

In general, if your program does not use state monads, but is just a simple, straightforward functional program, the combination of Haskabelle and Isabelle/HOL can work quite nicely without a big formal apparatus such as a pre/post calculus. You can just state properties directly as you might in quickcheck.

> It would be great if there exists a prover based on this kind of specifications. I already found the ESC/Haskell. Do you know some other works which could be interesting?

We're using Isabelle/HOL. In the work above this was together with our own translator from Haskell to Isabelle, in the future it will possibly Haskabelle which has already been pointed out.

Cheers,
Gerwin

Till Mossakowski

unread,

Oct 26, 2010, 6:38:43 AM10/26/10

to haskell@haskell.org >> "haskell@haskell.org"

The Heterogeneous Tool Set supports HasCASL for specification
of Haskell programs, and uses Isabelle for proving
http://www.dfki.de/sks/hets

Moreover, the Programatica project has an expressive logic
called P-logic, and tools supporting it:
http://programatica.cs.pdx.edu/

Best, Till

Simon Peyton-Jones

unread,

Oct 26, 2010, 6:43:52 AM10/26/10

to Till Mossakowski, haskell@haskell.org >> "haskell@haskell.org"

Would someone like to make a Haskell Wiki page to summarise the responses to this thread?

Simon

Peter Padawitz

unread,

Oct 26, 2010, 8:19:54 AM10/26/10

to Romain Demeyer, has...@haskell.org

Haskell functions may be verified interactively and/or automatically
with Expander2 (http://fldit-www.cs.uni-dortmund.de/~peter/Expander2.html
).

Induction, coinduction, narrowing and extendable sets of
simplification rules admit proofs and computations at various levels
of automation.

All derivations are recorded both in textual form and in terms of
straight-line programs that allow their stepwise replay.

Peter Padawitz
http://fldit-www.cs.tu-dortmund.de

Henk-Jan van Tuyl

unread,

Oct 31, 2010, 4:11:40 PM10/31/10

to Haskell mailing list, Simon Peyton-Jones

On Tue, 26 Oct 2010 12:43:36 +0200, Simon Peyton-Jones
<sim...@microsoft.com> wrote:

> Would someone like to make a Haskell Wiki page to summarise the
> responses to this thread?
>
> Simon
>

I have updated the page "Applications and libraries/Theorem provers" [0]
and created the new wiki page "Specification and proof" [1]. I hope
someone with more expertise on the subject will write the body of this new
page.

Regards,
Henk-Jan van Tuyl

[0]
http://www.haskell.org/haskellwiki/Applications_and_libraries/Theorem_provers
[1] http://www.haskell.org/haskellwiki/Specification_and_proof

--
http://Van.Tuyl.eu/
http://members.chello.nl/hjgtuyl/tourdemonad.html
--