HOL Redevelopment Project

The overall task is to make the open-source HOL4 system even better than it already is: to improve its speed by using a much better compiler, and to improve the user experience by allowing a modern Eclipse-based interface. There is some substantial re-engineering to be done to get to this goal.

Task 1: porting kernel

The kernel of the system needs to be ported from Moscow ML to the MLton compiler (both compilers for SML). This should be straightforward as the code has been written fairly portably.

Issues: identifying exactly where the kernel stops in the existing code-base.

Task 2: embedding Hamlet

The new system will need to support an interactive top-level loop for backwards compatibility. This will need to be the interactive implementation of SML called Hamlet, extended with theorem-proving primitives drawn from the kernel (see Task 1).

Issues: embedding the new primitives into Hamlet might be tricky.

Task 3: porting non-kernel to Hamlet

The remainder of the existing HOL4 code base, will have to run in the embedded interpreter. This again should be easy as the Hamlet and Moscow ML systems should have the same notions of what it is to be SML.

Issues: none obvious

Task 4: integrating new theory file format

Abhiti Barthwal’s current (2005–2006) Honours project is developing a new theory file format for HOL. This is promising work and should be straightforward to include. However, one Honours project (due to be done in mid 2006) is not going to be a complete story, so more work on file format will likely be needed here.

Task 5: linking to Eclipse

In collaboration with the ProofGeneral plug-in for Eclipse, write a tool to display ongoing proofs from inside Eclipse. There will be some sort of link between proof manipulation tools in SML to the Java-based display in the IDE.

Further reading

There is some discussion of this task on the MLton mailing list. See: