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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
