2011/6/21 Jason Dagit
> On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger
> wrote:
> > Hello Haskell fellows,
> >
> > recently there has been a huge progress in generating real programs by
> > specifying them in interactive theorems prover like Isabelle or Coq,
be to
build something like CompCert the other way around (in this case writing a C
compiler in SML and proving its correctness?)
Best regards,
Uli Kastlunger
[0] http://compcert.inria.fr/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http
