[Haskell-cafe] Verifying Haskell Programs

[Austin Seipp]

Excerpts from Paulo J. Matos's message of Tue Feb 03 02:31:00 -0600 2009:
> Any references to publications related to this?

While it's not Haskell, this code may be of interest to you:

http://pauillac.inria.fr/~xleroy/bibrefs/Leroy-compcert-06.html

This paper is about the development of a compiler backend using the
Coq proof assistant, which takes Cminor (a C-like language) and
outputs PowerPC assembly code. Coq is used both to program the
compiler and prove it is correct.

Austin