Deriving mixed evaluation from standard evaluation for a simple functional language

John Hannan, Dale Miller

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationMathematics of Program Construction - 375th Anniversary of the Groningen University International Conference, Proceedings
EditorsJan L.A. van de Snepscheut
PublisherSpringer Verlag
Pages239-255
Number of pages17
ISBN (Print)9783540513056
DOIs
Publication statusPublished - Jan 1 1989
EventConference on Mathematics of Program Construction at the occasion of the university's 375th anniversary, 1989 - Groningen, Netherlands
Duration: Jun 26 1989Jun 30 1989

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume375 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherConference on Mathematics of Program Construction at the occasion of the university's 375th anniversary, 1989
CountryNetherlands
CityGroningen
Period6/26/896/30/89

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Hannan, J., & Miller, D. (1989). Deriving mixed evaluation from standard evaluation for a simple functional language. In J. L. A. van de Snepscheut (Ed.), Mathematics of Program Construction - 375th Anniversary of the Groningen University International Conference, Proceedings (pp. 239-255). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 375 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-51305-1_13