This unit centres around the HOL theorem proving system. HOL is one of a family of theorem provers that share a common design called the `LCF architecture'. The LCF architecture is so named because its first use was in a theorem prover called LCF. Users of LCF architecture tools prove theorems in the logic supported by the tool (the object language) by writing programs to construct a proof using a programming language (the meta-language). ML is a programming language that began life is the meta-language of the original LCF system, hence the name. ML is a general-purpose programming language, which has evolved over time, and is now used in a variety of application areas.
ML is a functional programming language, and as such it has much in common with languages like Miranda and Haskell. It is distinguished from these languages in two ways: ML uses strict evaluation rather than lazy evaluation (although a lazy dialect of ML does exist); and ML is not a `pure' functional language, you can also write imperative programs in ML. A functional language in which you can write imperative programs sounds a bit like Lisp or Scheme, but ML differs from these languages by enforcing a strong type discipline, an essential feature for its application in LCF theorem provers.
There are a variety of ML dialects in existence, worse still, there are a variety of versions of the HOL theorem prover - each based on a different dialect of ML! We will be using HOL98, the latest version of HOL. Moscow ML is the meta-language of HOL98, so for this unit ML usually means Moscow ML.
Moscow ML is a subset of Standard ML, or SML, the most popular dialect of ML. Standard ML is partitioned in to the Core language, the Modules language, and the Basis library. Moscow ML supports the complete Core language, some of the Modules language, and most of the Basis library. The omissions won't worry us because we won't be writing large programs. Any book or other documentation you find about Standard ML will also be of use with Moscow ML.
Most of the differences between the various ML dialects are cosmetic. For this reason people don't usually bother to rewrite the HOL documentation when they port HOL to a different ML dialect. Most of the HOL98 documentation comes straight from HOL88, a version of HOL written in the original dialect of ML - now known as Classic ML. Classic ML is every bit as dead as Classic Coke isn't, but you'll have to get a bit of a feel for Classic ML so you can understand how to use the examples in the documentation with the current version of HOL. Relax, this is easier than it sounds.
Moscow ML is available for a wide variety of platforms. If you also want to get HOL for your computer you will need Moscow ML version 1.43, the current version. Precompiled binary distributions of Moscow ML without source code are available for some operating systems, like Linux, but you will need a version with full source code to build HOL. You can download Moscow ML from the Moscow ML home page.
The moderated news group comp.lang.ml is dedicated to the various dialects of ML and their compilers. Its a friendly group with low trafic, so you can ask questions there without fear of flaming.
An ML Frequently Asked Questions List is archived on the web, and posted to comp.lang.ml semi-regularly.