A Staging Calculus and its Application to the Verification of Translators

Abstract

We develop a calculus in which the computation steps required to execute a computer program can be separated into discrete stages. The calculus, denoted λ2, is embedded within the pure untyped λ-calculus. The main result of the paper is a characterization of sufficient conditions for confluence for terms in the calculus. The condition can be taken as a correctness criterion for translators that perform reductions in one stage leaving residual redexes over for subsequent computation stages. As an application of the theory, we verify the correctness of a macro expansion algorithm. The expansion algorithm is of some interest in its own right since it solves the problem of desired variable capture using only the familiar capture avoiding substitutions.