[Haskell-cafe] Verifying Haskell Programs

Austin Seipp mad.one at gmail.com
Tue Feb 3 04:40:47 EST 2009

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:


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.


More information about the Haskell-Cafe mailing list