Program Verification Using Higher Order Logic
A. Cant · Defense Technical Information Center (DTIC) · 1992
This paper describes a number of experiments in program verification carried out within two automated proof assistants, namely the HOL (High Order Logic) system and Isabelle. Various approaches to programming language semantics are described. Theories and tactics for proving the correctness of programs written in small functional and imperative languages are then constructed within HOL and Isabelle.