Functional Back-Ends within the Lambda-Sigma Calculus

Thérèse Hardin 1 Luc Maranget 1 Bruno Pagano
1 PARA - Parallélisme
Inria Paris-Rocquencourt
Abstract : We define a weak lambda-calculus, lambda-sigma-w, as a subsystem of the full lambda-calculus with explicit substitutions lambda-sigma-lift. We claim that lambda-sigma-w could be the archetypal output language of functional compilers, just as the lambda-calculus is their universal input language. Furthermore, lambda-sigma-lift 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.
Type de document :
Rapport
[Research Report] RR-3034, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073659
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:26:03
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:20:46

Fichiers

Identifiants

  • HAL Id : inria-00073659, version 1

Collections

Citation

Thérèse Hardin, Luc Maranget, Bruno Pagano. Functional Back-Ends within the Lambda-Sigma Calculus. [Research Report] RR-3034, INRIA. 1996. 〈inria-00073659〉

Partager

Métriques

Consultations de la notice

135

Téléchargements de fichiers

165