Compilation of extended recursion in call-by-value functional languages

TL;DR

This paper presents a formalization and correctness proof of a compilation scheme for mutually-recursive definitions in call-by-value functional languages, enabling a broader range of recursive constructs than prior methods.

Contribution

It introduces a novel translation scheme to a lambda-calculus with in-place memory updates, extending the support for recursive definitions in functional language compilation.

Findings

The translation scheme is proven correct.

Supports a wider class of recursive definitions.

Formalizes the compilation process with proofs.

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.