The Machine-Assisted Proof of Programming Language
Properties
Ph.D. Thesis
Myra VanInwegen
Ph.D. Thesis. Univ. of
Pennsylvania Computer and Information Science Tech Report
MS-CIS-96-31, December 1996.
Abstract
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.
Available in compressed PS format.
Myra's Home Page