Functional runtime systems within the lambda-sigma calculus

TLDR

The paper introduces λσ w, a weak λ‑calculus with explicit substitutions, as a subsystem of the full λ‑calculus. The authors propose that λσ w serves as an archetypal output language for functional compilers and that λσ [uArr ] provides a suitable theory for proving compiler correctness. They demonstrate this by formally proving correctness of four simplified compilers and runtime systems—Krivine, SECD, FAM, and CAM—modeled as abstract machines. The study provides the first formal proofs of Cardelli's FAM and its compiler.

Abstract

We define a weak λ-calculus, λσ w , as a subsystem of the full λ-calculus with explicit substitutions λσ [uArr ] . We claim that λσ w could be the archetypal output language of functional compilers, just as the λ-calculus is their universal input language. Furthermore, λσ [uArr ] could be the adequate theory to establish the correctness of functional compilers. Here we illustrate these claims by proving the correctness of four simplified compilers and runtime systems modelled as abstract machines. The four machines we prove are the Krivine machine, the SECD, the FAM and the CAM. Thus, we give the first formal proofs of Cardelli's FAM and of its compiler.