Submitted to the Journal of Automated Reasoning Special Issue on Formal Proof, January 1997. The paper wasn't accepted, but still may prove useful as a much shorter synpopsis of my thesis work.
We describe the use of the theorem prover HOL to prove properties of the Core subset of the programming language SML. We proved properties of evaluation and the type system, including determinism of evaluation and a collection of substitution lemmas for the type system. We made substantial progress towards proving type preservation. On the whole the benefits of using HOL greatly outweighed the drawbacks: we believe that these theorems could not been proved in the amount of time taken by this project had we not used mechanized help.
Available in compressed PS or compressed DVI format.