Declarative theorem proving for operational semantics
Donald Robert Syme · Apollo (University of Cambridge) · 1999
This dissertation is concerned with techniques for formally checking properties of systems that are described by operational semantics. We describe innovations and tools for tackling this problem, and a large case study in the application of these tools. The innovations centre on the notion of \declarative theorem proving, and in particular techniques for declarative proof description. We de ne what we mean by this, assess its costs and bene ts, and describe the impact of this approach with respect to four fundamental areas of theorem prover design: speci cation, proof description, automated reasoning and interaction. We have implemented our techniques as the Declare system, which we use to demonstrate how the ideas translate into practice. The case study is a formally checked proof of the type soundness of a subset of the Java language, and is an interesting result in its own right. We argue why declarative techniques substantially improved the quality of the results achieved, particularly with respect to maintainability and readability. Declaration This dissertation is the result of my own work and includes nothing which is the outcome of work done in collaboration. xi