Download Now Free registration required
This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than previous methods. The authors formalize the technique as a translation scheme to a lambda-calculus featuring in-place update of memory blocks, and prove the translation to be correct. Functional languages usually feature mutually recursive definition of values, for example via the letrec construct in Scheme, letrec in Caml, val rec and fun in Standard ML, or recursive equations in Haskell. Beyond syntax, functional languages differ also in the kind of expressions they support as right-hand sides of mutually recursive definitions.
- Format: PDF
- Size: 471.25 KB