@inproceedings{b95fd71d641c4a83be9b1bb5048cd757,
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",
month = jan,
day = "1",
doi = "10.1007/3-540-51305-1\_13",
language = "English",
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",
}