3 Feb
2009
3 Feb
'09
4:40 a.m.
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