@inproceedings{a4de82fdf5ae4102b97df28f30d28cb8,
title = "Interpreter verification for a functional language",
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.",
author = "Manfred Broy and Ursula Hinkel and Tobias Nipkow and Christian Prehofer and Birgit Schieder",
note = "Publisher Copyright: {\textcopyright} 1994, Springer Verlag. All rights reserved.; 14th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1994 ; Conference date: 15-12-1994 Through 17-12-1994",
year = "1994",
doi = "10.1007/3-540-58715-2_115",
language = "English",
isbn = "9783540587156",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "77--88",
editor = "P.S. Thiagarajan",
booktitle = "Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings",
}