From call-by-value to interaction by typed closure conversion

Abstract

We study the efficient implementation of call-by-value using the structure of interactive computation models. This structure has been useful in applications to resource-bounded compilation, but much of the existing work in this area has focused on call-by-name programming languages. This paper works towards the goal of a simple, efficient treatment of call-by-value languages. In previous work we have studied cps-translation as an approach to implementing call-by-value and have observed that it needs to be refined in order to achieve efficient space usage. In this paper we give an alternative presentation of the refined translation, which is close to existing methods of typed closure conversion. We show that a simple correctness proof following Benton and Hur is possible for this formulation. Moreover, we extend previous work to cover full recursion in the source language.