The machine-assisted proof of programming language properties

The goals of the project described in this thesis are twofold. First, we wanted to demonstrate that if a programming language has a semantics that is complete and rigorous (mathematical), but not too complex, then substantial theorems can be proved about it. Second, we wanted to assess the utility of using an automated theorem prover to aid in such proofs. We chose SML as the language about which to prove theorems: it has a published semantics that is complete and rigorous, and while not exactly simple, is comprehensible. We encoded the semantics of Core SML into the theorem prover HOL (creating new definitional packages for HOL in the process). We proved important theorems about evaluation and about the type system. We also proved the type preservation theorem, which relates evaluation and typing, for a good portion of the language. We were not able to complete the proof of type preservation because it is not true: we found counterexamples. These proofs demonstrate that a good semantics will allow the proof of programming language properties and allow the identification of trouble spots in the language. The use of HOL had its plusses and minuses. On the whole the benefits greatly outweigh the drawbacks, enough so that we believe that these theorems could not been proved in amount of time taken by this project had we not used automated help