Interpreter Verification for a Functional Language

. Starting from a denotational and a term-rewriting based operational semantics (an interpreter) for a small functional language, we present a correctness proof of the interpreter w.r.t. the denotational semantics. The complete proof has been formalized in the logic LCF and checked with the theorem prover Isabelle. Based on this proof, conclusions for mechanical theorem proving in general are drawn. 1 Introduction Compiler and interpreter verification is a key component in the correctness argument for any software system written in a high-level language. Otherwise the carefully verified high-level programs might be compiled or interpreted incorrectly. Proving the correctness of machine oriented programs [3] instead may be inevitable for some applications, but is methodologically a step backwards. Verification of compilers and interpreters is also challenging from a theoretical point of view because complex semantical questions are involved [5, 6]. These comprise the formalizati..