Department of Informatics

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

TUM
 
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
Year:1994
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.
 
BibTeX

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