|
The Tail-Recursive SECD Machine
1999 Award Winner
John D.Ramsdell, The MITRE Corporation
ABSTRACT
One method for producing verified implementations of programming languages is to formally derive them from abstract machines.Tail-recursive abstract machines provide efficient support for iterative processes via the ordinary procedure all mechanism.This document argues that the use of tail-recursive abstract machines incurs only a small increase in theorem-proving burden when compared with what is required when using ordinary abstra t ma hines.The position is supported by comparing orrectness proofs performed using the Boyer-Moore theorem prover.
A by-product of this effort is a syntactic criterion based on tail contexts for identifying which procedure calls must be implemented as tail calls.The concept of tail contexts was used in the latest Scheme Report, the only language specification known to the author that defines the requirement that its implementations must be tail recursive.
» Download Paper [PDF, 291KB]
Publication
Published in 1999 ©Kluwer Academic Publishers. Journal of Automated Reasoning, Vol. 23, pp. 43-62.
Additional Search Keywords
tail recursion, tail call, SECD machine, CEK machine, verified implementation, Boyer-Moore theorem prover
|
