[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it

[Stephen Weeks]

> I guess you are suggesting the use of a series of executables.  

Yep.  Your explanation fills it in nicely.

> If users wanted to include code of their own, they would create
> their own monoliths.

Yes.  The thing to keep in mind is that whatever you want to run fast
all has to be SML source in the same program.  In your (or your
users') case, that means the HOL kernel and any accompanying theory
code.

> Now we just need that embedded SML interpreter for our script (=
> theory-generation) files.

Maybe Hamlet?  Andreas reads this list; perhaps he could comment.