A Derived Reasonable Abstract Machine for Strong Call by Value

We present an efficient implementation of the full-reducing call-by-value strategy for the pure λ-calculus in the form of an abstract machine. The presented machine has been systematically derived using Danvy et al.’s functional correspondence that connects higher-order interpreters with abstract-machine models by a well-established transformation technique. It improves on a previously presented machine by Biernacka et al. in terms of efficiency: the new machine simulates β-reduction with the overhead polynomial in the number of β-steps and in the size of the initial term. Thus, the machine makes a “reasonable” (in the sense of Accattoli et al.) implementation of Strong CbV. We prove correctness and reasonability of the machine. The latter property is shown using a form of amortized cost analysis à la Okasaki.