TY - GEN
T1 - Deriving mixed evaluation from standard evaluation for a simple functional language
AU - Hannan, John
AU - Miller, Dale
N1 - Funding Information:
Acknowledgements: The first author is supported in part by a fellowship from the Corporate Research and Architecture Group, Digital Equipment Corporation, Maynard, MA USA. Both authors are supported in part by grants NSF CCR-87-05596, ONR N00014-88-K-0633, and DARPA N00014-85-K-0018.
Publisher Copyright:
© 1989, Springer-Verlag.
PY - 1989
Y1 - 1989
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84976825461&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84976825461&partnerID=8YFLogxK
U2 - 10.1007/3-540-51305-1_13
DO - 10.1007/3-540-51305-1_13
M3 - Conference contribution
AN - SCOPUS:84976825461
SN - 9783540513056
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 239
EP - 255
BT - Mathematics of Program Construction - 375th Anniversary of the Groningen University International Conference, Proceedings
A2 - van de Snepscheut, Jan L.A.
PB - Springer Verlag
T2 - Conference on Mathematics of Program Construction at the occasion of the university's 375th anniversary, 1989
Y2 - 26 June 1989 through 30 June 1989
ER -