Department of Informatics

TU München - Fakultät für Informatik
Chair IV: Software & Systems Engineering

PDF-Datei  Interpreter Verification for a Functional Language

Conference Paper

Author:Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder
Conference:Proc. 14th Conf. Foundations of Software Technology and Theoretical Computer Science
Editor:P.S. Thiagarajan
Pages:77 - 88
Abstract: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.

(c) 1999-2006 - Lehrstuhl Software & Systems Engineering
Sitemap |  Contact