Variable elimination for building interpreters

TL;DR

This paper presents a method for building interpreters by reusing host language functions through combinatory logic, providing a mechanically verified correctness proof for call-by-value strategies with imperative features.

Contribution

It introduces a novel approach to interpreter construction using combinatory logic and offers a formal correctness proof for this method.

Findings

Reusing host language functions simplifies interpreter implementation.

The approach is proven correct for call-by-value with imperative features.

Mechanically checked proof ensures reliability of the transformation.

Abstract

In this paper, we build an interpreter by reusing host language functions instead of recoding mechanisms of function application that are already available in the host language (the language which is used to build the interpreter). In order to transform user-defined functions into host language functions we use combinatory logic : lambda-abstractions are transformed into a composition of combinators. We provide a mechanically checked proof that this step is correct for the call-by-value strategy with imperative features.