Get HLM at Fast, secure and Free Open Source software downloads

The HLM Proof Assistant


Click here to download the HLM prototype and library.

(Last update: February 8, 2011)

Note: This prototype is intended as a proof of concept; it cannot be used as an actual proof assistant yet. Also, most of the library has been written manually in XML, and cannot be reproduced in the GUI yet.


Extract hlm.jar and swt.jar into the same directory, then run hlm.jar as follows:

Then extract library.hlm to a writable directory and open it in HLM.

SVN Access

Check out both the source code and the library from:

The easiest way to compile HLM is from the Eclipse IDE. First set up a classpath variable SWT pointing at the appropriate .jar file somewhere in the Eclipse directory (because Eclipse uses SWT). Then choose "File / Import / Existing projects into workspace," select the java subdirectory of HLM as the root directory, and import all projects it contains. This should also import some run configurations that can be accessed via "Run / Run configurations."

In the GUI, load the file Library.xml from the library subdirectory.