Functional back-ends within the lambda-sigma calculus

TLDR

λσw is proposed as the archetypal output language of functional compilers, with λσ⇑ serving as an adequate theory for proving correctness of simplified functional compilers. The authors aim to illustrate these claims by proving the correctness of two simplified compilers and runtime systems modeled as abstract machines. They define a weak λ‑calculus λσw with explicit substitutions, present the Krivine machine, and provide the first formal proofs of Cardelli's FAM and its compiler. They prove the correctness of two simplified compilers and runtime systems modeled as abstract machines, including 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 λσ⇑. We claim that λσw could be the archetypal output language of functional compilers, just as the λ-calculus is their universal input language. Furthermore, λσ⇑ could be the adequate theory to establish the correctness of simplified functional compilers. Here, we illustrate these claims by proving the correctness of two simplified compilers and runtime systems modeled as abstract machines. We first present the Krivine machine. Then, we give the first formal proofs of Cardelli's FAM and of its compiler.