[Yhc] Verified compiler

[Neil Mitchell]

Hi William,

> As you are compiler experts, I am asking your help.
You may overestimate our compiler skills :)

> If somebody is interested in functional programming and in formal methods to
> help to implement a verified compiler , he is welcome :)
I saw you giving out a list of sources in the haskell mailing list as
well, however you missed:

Catch: http://www-users.cs.york.ac.uk/~ndm/projects/catch.php
ESC/Haskell: http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps

[Note, I am the one who does Catch, so considered that a biased plug]

> Haskell also depends on a complicated run-time system. Such run-time systems
> are often unverified. Implementing a minimal, high-assurancerun-time system
> is a topic for future work.
The runtime for Yhc is relatively simple - probably the simplest and
cleanest of any of the Haskell implementations. The compiler is
probably not a good start to build a high assurance system :)

Thanks, and good luck!

Neil