Abstract
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. We formalize our technique as a translation scheme to a lambda-calculus featuring in-place update of memory blocks, and prove the translation to be correct. © 2009 Springer Science+Business Media, LLC.
| Original language | English |
|---|---|
| Pages (from-to) | 3-66 |
| Number of pages | 64 |
| Journal | Higher-Order and Symbolic Computation |
| Volume | 22 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - Mar 2009 |
Keywords
- Compilation
- Functional languages
- Recursion
- Semantics