Interpreter Verification for a Functional Language
Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit
Schieder
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 mechanically with the
help of the theorem prover Isabelle. This substantial proof is analyzed in
some detail and conclusions for mechanical theorem proving in general are
drawn.
dvi
SpringerLink
BibTeX:
<![CDATA[
@inproceedings{BroyHNPS-94,
author={Manfred Broy and Ursula Hinkel and Tobias Nipkow and
Christian Prehofer and Birgit Schieder},
title={Interpreter Verification for a Functional Language},
booktitle={Proc.\ 14th Conf.\ Foundations of Software Technology and
Theoretical Computer Science},
editor={P.S. Thiagarajan},
publisher=Springer,series=LNCS,volume=880,year=1994,pages={77--88}}
]]></plaintext></p></div></div>