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. A description of what you need and how to install it can be found in Exercise 1.

Andreas Linder ( created a Docker container for HOL. It can be found on I myself am unable to help with getting it running, but Andreas can help if you want to use it and have trouble! Thanks Andreas!

Feedback News