### 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 language | English (US) |
---|---|

Title of host publication | Mathematics of Program Construction - 375th Anniversary of the Groningen University International Conference, Proceedings |

Editors | Jan L.A. van de Snepscheut |

Publisher | Springer Verlag |

Pages | 239-255 |

Number of pages | 17 |

ISBN (Print) | 9783540513056 |

DOIs | |

Publication status | Published - Jan 1 1989 |

Event | Conference on Mathematics of Program Construction at the occasion of the university's 375th anniversary, 1989 - Groningen, Netherlands Duration: Jun 26 1989 → Jun 30 1989 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 375 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | Conference on Mathematics of Program Construction at the occasion of the university's 375th anniversary, 1989 |
---|---|

Country | Netherlands |

City | Groningen |

Period | 6/26/89 → 6/30/89 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*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