Hostname: page-component-cd9895bd7-p9bg8 Total loading time: 0 Render date: 2024-12-26T05:21:48.749Z Has data issue: false hasContentIssue false
  • English
  • Français

Functional runtime systems within the lambda-sigma calculus

Published online by Cambridge University Press:  01 March 1998

THÉRÈSE HARDIN ,
LUC MARANGET  and
BRUNO PAGANO
THÉRÈSE HARDIN
Affiliation:
LIP6, Université Pierre et Marie Curie, 75252 Paris Cedex 05, France, INRIA Rocquencourt, BP 105, 78153 Le Chesnay Cedex, France (e-mail: [email protected])
LUC MARANGET
Affiliation:
INRIA Rocquencourt, BP 105, 78153 Le Chesnay Cedex, France (e-mail: [email protected])
BRUNO PAGANO
Affiliation:
LIP6, Université Pierre et Marie Curie, 75252 Paris Cedex 05, France (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Information
Journal of Functional Programming , Volume 8 , Issue 2 , March 1998 , pp. 131 - 176
Copyright
© 1998 Cambridge University Press

Footnotes

This work was partially supported by the ESPRIT Basic Research Project 6454–CONFER.
Submit a response

Discussions

No Discussions have been published for this article.