[MLton] Isabelle on MLton?
Fri, 24 Mar 2006 14:03:32 -0500 (EST)
> Is there any chance that we will be able to use MLton to run Isabelle
> (isabelle.in.tum.de) in the forseeable future? We need an interactive
> top-level, which I believe you currently don't support.
> At the moment we use PolyML (mostly) and sml/nj.
If the interactive top-level is a requirement for Isabelle, then the short
answer is "no", since there are no plans on adding a REPL in the
Of course, one might consider not using the host ML type-system/REPL as
the means of theorem checking and interaction; instead, roll an embedded
interpreter of one form or another.
We had a lengthy discussion with some of the HOL (hol.sourceforge.net)
developers approximately a year ago:
Are there specific aspects of the interactive top-level that are required