Functional back-ends within the lambda-sigma calculus

We define a weak lambda-calculus, lambda sigma(omega), as a subsystem of the full lambda-calculus with explicit substitutions lambda sigma double up arrow. We claim that lambda sigma(omega) could be the archetypal output language of functional compilers, just as the lambda-calculus is their universal input language. Furthermore, lambda sigma double up arrow 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.