@inproceedings{a9c8dbac472141c4916da3b11088484b,
title = "Deriving mixed evaluation from standard evaluation for a simple functional language",
abstract = "We demonstrate how a specification for the standard evaluation of a simple functional programming language can be systematically extended to a specification for mixed evaluation. Using techniques inspired by natural semantics we specify a standard evaluator by a set of inference rules. The evaluation of programs is then performed by a restricted kind of theorem proving in this logic. We then describe a systematic method for extending the proof system for standard evaluation to a new proof system that provides greater flexibility in treating bound variables in the object-level functional programs. We demonstrate how this extended proof system provides the capabilities of a mixed evaluator and how correctness with respect to standard evaluation can be proved in a simple and direct manner. The current work focuses only on a primitive notion of mixed evaluation for a simple functional programming language, but we believe that our methods will extend to more sophisticated kinds of evaluations and richer languages.",
author = "John Hannan and Dale Miller",
note = "Publisher Copyright: {\textcopyright} 1989, Springer-Verlag.; Conference on Mathematics of Program Construction at the occasion of the university's 375th anniversary, 1989 ; Conference date: 26-06-1989 Through 30-06-1989",
year = "1989",
doi = "10.1007/3-540-51305-1_13",
language = "English (US)",
isbn = "9783540513056",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "239--255",
editor = "{van de Snepscheut}, {Jan L.A.}",
booktitle = "Mathematics of Program Construction - 375th Anniversary of the Groningen University International Conference, Proceedings",
address = "Germany",
}