certifying compilation using MLton

[Robert Harper]

Hi Steve:

Thanks for the followup note.  Actually, you're confusing two different
efforts.

Leaf Petersen is doing a thesis on making TILT into a certifying compiler.
His proposal is available on my web page, under Students.  This work doesn't
involve MLTon at all, though any advice you may have is certainly welcome.
His email address is leaf@cs.cmu.edu.

Joshua Dunfield, who I told you about in Florence, built a certifying
compiler for Standard ML by a tour de force application of "software duct
tape", starting with MLTon to generate RML, an intermediate language that
Tolmach and Oliva devised, then compiling RML to Popcorn (via a few good
tricks), which then yields TAL.  I recall that you thought we could
streamline this by using the MLTon IL, rather than RML, which could well be
the case.  Joshua chose RML because he'd already worked with it as an
undergraduate at Portland State, and hence felt more confident about getting
something going fast.  Joshua is joshuad@cs.cmu.edu.  I'm sure he'd be very
happy to tell you about what he did, and would be glad for your advice.

Bob

-----Original Message-----
From: Stephen Weeks [mailto:sweeks@intertrust.com]
Sent: Thursday, September 27, 2001 4:56 PM
To: Robert Harper
Cc: MLton@sourcelight.com
Subject: certifying compilation using MLton



Hi Bob.  Seeing Leaf's proposal announcement reminded me of your mention at
ICFP
of a student that was using MLton for a proof of concept of certifying
compilation.  I don't remember if it was Leaf or another student, but I
wanted
to remind you to please tell them to get in touch with us
(MLton@sourcelight.com), as we'd be interested to hear what they did and if
we
could help out with any questions or future plans they might have.  Thanks.