Software needed

In the Interactive Theorem Proving course, the HOL theorem prover is used. For the practical part, you will need to have HOL installed. For this you need.

Standard ML

You will need to have standard ML available. Please install PolyML 5.6 or later (download,webpage).

HOL

Please install a recent version of the HOL theorem prover. I recomment installing the most recent version from the git repository. If for some reason you don't want to do this, the latest release should be fine as well. Installation instructions can be found on HOL's webpage.

Emacs

In the lecture emacs will be used as a user/interface. Please install a recent version of Emacs. Activate the hol-mode. For details how to do it, please look at it's documentation.

SML mode

To enable syntax highlighting for ML, please install the SML mode.

If you have questions, please contact Thomas Tuerk.