Functional Back-Ends within the Lambda-Sigma Calculus

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