This research into automatic theorem proving, program verification and mechanization of mathematical reasoning will be carried out over a period of three years. The basis is the study of logical formalisms for program verification and mathematical reasoning. This includes metamathematical reasoning and the proof checker (implemented at Stanford under NSF grant MCS-8206565) intensional semantics of programming languages and use of theorem proving tools to formalize semantics as a basis for proving intensional and extensional properties of programs and for mechanizing (aspects of) programming activities such as specification, transformation, and modification. the formalisms under study will be implemented using a common software platform. This software will be formally specified and proved to meet its specifications by the techniques to be investigated under the grant.
