[Haskell-cafe] Verifying Haskell Programs
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