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


@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}}