More Web Proxy on the site http://driver.im/

Article

Free access

Functional back-ends within the lambda-sigma calculus

Authors:

Thérèse Hardin,

Bruno PaganoAuthors Info & Claims

ICFP '96: Proceedings of the first ACM SIGPLAN international conference on Functional programming

Pages 25 - 33

https://doi.org/10.1145/232627.232632

Published: 15 June 1996 Publication History

Abstract

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 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.

References

[1]

M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Ldvy} "Explicit Substitutions", POPL'90.

Digital Library

[2]

A. W. Appel, "Compiling with Continuations", Cambridge University Press, 1992.

Digital Library

[3]

Z. Ariola, M. Feleisen. J. Maraist, M. Odersky, and P. Wadler, "A call-by-need lambda-calcuhs". POPL'95.

Digital Library

[4]

A. Asperti, "A CategoricM Understanding of Environmeat Machines", JFP, 2(1), 1992.

[5]

L. Augustsson, "A Compiler For Lazy ML", LFP'84.

Digital Library

[6]

L. Cardelli, "Compiling a Functional Lang~age", LFP'84.

Digital Library

[7]

G. Cousineau, P.-L. Curien and M. Mauny, "The CategoricM Abstract Machine", FPCA'85.

Digital Library

[8]

P. Cr~gut, "An Abstract Machine for the NormMization of Lambda-terms", LFP'90.

Digital Library

[9]

P.-L. Curien, "An Abstract Framework for Environment Machines", TCS. 82, 1991.

Digital Library

[10]

P.-L. Curien, T. Hardin and J.-J. L~vy, "Confluence Properties of Weak and Strong CMculi of Explict Substitutions'', iNRIA Research Report No 1617, 1992. Also to appear in JACM in april 1996.

Digital Library

[11]

R. Douence and P. Fradet, "Towards a Taxonomy of FunctionM Language Implementations". PILP'95.

Digital Library

[12]

G. Dowek, T. Hardin and C.Kirchner, "Higher-Order Unitication via explicit Substitutions", LICS'95.

Digital Library

[13]

J. Fairbairn and S. Wray, "Tim: A Simple, Lazy Abstract Machine to Execute Supercombinators', FPCA'87.

Digital Library

[14]

J. Hannan, D. Miller, "From Operational Semantics to Abstract Machines", Journal of Mathematical Structures in Computer Science, 2(4):415-459, 1992

[15]

H. Herbelin, "A A-CMculas Structure Isomorphic to Sequent Calculus Structure", CSL'94.

Digital Library

[16]

P. J. Landin, "The MechanicM Evaluation of Expressions", Computer Journal, Vol 6, No 4, 1964.

[17]

J. Launchbury, "A NaturM Semantics for Lazy Evaluation'', POPL'93.

Digital Library

[18]

X. Leroy, "The ZINC Experiment: An EconomicM Implementation of the ML Language", INRIA Technical Report 117, 1990.

[19]

P. Lescanne, "From Act to Av: a Journey through Calculi of Explicit Substitutions", POPL'94.

Digital Library

[20]

L. Maranget, "OptimM derivation in Orthogonal Rewriting Systems and in Weak Lambda Calcul?', POPL'91.

[21]

B. Pagano, "Bi-simulation de machines abstraites ell lambda-sigma-calcur', Journdes Francophone des Langages Applicatifs 1995, INRIA Editions (In french).

[22]

G.D. Plotkin, "LCF Considered as a Programming Language''. TCS, 5:225-255, 1977.

[23]

$. L. Peyton Jones, "The implementation of Functional Programming Languages", Prentice-Hall, 1987.

Digital Library

[24]

M. Rittri, "Proving the Correctness of a VirtuM Machine by a Bisimulation", Phd thesis, University of G6teborg and Chalmers University of Technology, 1988.

Cited By

Palmer ZFilardo NWu K(2024)Intensional FunctionsProceedings of the ACM on Programming Languages10.1145/36897148:OOPSLA2(87-112)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689714
Bello JSilva CNov ODubois RArora ASalamon JMydlarz CDoraiswamy H(2019)SONYCCommunications of the ACM10.1145/322420462:2(68-77)Online publication date: 28-Jan-2019
https://dl.acm.org/doi/10.1145/3224204
Herlihy M(2019)Blockchains from a distributed computing perspectiveCommunications of the ACM10.1145/320962362:2(78-85)Online publication date: 28-Jan-2019
https://dl.acm.org/doi/10.1145/3209623
Show More Cited By

Index Terms

Functional back-ends within the lambda-sigma calculus

Recommendations

Functional back-ends within the lambda-sigma calculus

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 ...
Functional runtime systems within the lambda-sigma calculus

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. ...
Linear lambda calculus with non-linear first-class continuations
ICSCA '17: Proceedings of the 6th International Conference on Software and Computer Applications

The Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '96: Proceedings of the first ACM SIGPLAN international conference on Functional programming

June 1996

273 pages

ISBN:0897917707

DOI:10.1145/232627

Chairman:
Robert Harper
Carnegie Mellon Univ., Pittsburgh, PA
,
Editor:
Richard L. Wexelblat

ACM SIGPLAN Notices Volume 31, Issue 6
June 15, 1996
273 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/232629
Chairmen:
Robert Harper
Carnegie Mellon Univ., Pittsburgh, PA
,
Richard L. Wexelblat
Issue’s Table of Contents

Copyright © 1996 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 June 1996

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ICFP96

Sponsor:

SIGPLAN

ICFP96: International Conference on Functional Programming

May 24 - 26, 1996

Pennsylvania, Philadelphia, USA

Acceptance Rates

ICFP '96 Paper Acceptance Rate 25 of 83 submissions, 30%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

46
Total Citations
View Citations
450
Total Downloads

Downloads (Last 12 months)93
Downloads (Last 6 weeks)14

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Palmer ZFilardo NWu K(2024)Intensional FunctionsProceedings of the ACM on Programming Languages10.1145/36897148:OOPSLA2(87-112)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689714
Bello JSilva CNov ODubois RArora ASalamon JMydlarz CDoraiswamy H(2019)SONYCCommunications of the ACM10.1145/322420462:2(68-77)Online publication date: 28-Jan-2019
https://dl.acm.org/doi/10.1145/3224204
Herlihy M(2019)Blockchains from a distributed computing perspectiveCommunications of the ACM10.1145/320962362:2(78-85)Online publication date: 28-Jan-2019
https://dl.acm.org/doi/10.1145/3209623
Nishizaki SNarita KUeda T(2015)Simplification of Abstract Machine for Functional Language and Its Theoretical InvestigationJournal of Software10.17706/jsw.10.10.1148-115910:10(1148-1159)Online publication date: 2015
https://doi.org/10.17706/jsw.10.10.1148-1159
Narita KNishizaki SMizuno T(2010)A simple abstract machine for functional first-class continuations2010 10th International Symposium on Communications and Information Technologies10.1109/ISCIT.2010.5664903(111-114)Online publication date: Oct-2010
https://doi.org/10.1109/ISCIT.2010.5664903
Ariola ZBohannon ASabry A(2009)Sequent calculi and abstract machinesACM Transactions on Programming Languages and Systems10.1145/1516507.151650831:4(1-48)Online publication date: 26-May-2009
https://dl.acm.org/doi/10.1145/1516507.1516508
Taylor BAzadegan S(2008)Moving beyond security tracksACM SIGCSE Bulletin10.1145/1352322.135224640:1(320-324)Online publication date: 12-Mar-2008
https://dl.acm.org/doi/10.1145/1352322.1352246
Bailey MColeman CDavidson J(2008)Defense against the dark artsACM SIGCSE Bulletin10.1145/1352322.135224540:1(315-319)Online publication date: 12-Mar-2008
https://dl.acm.org/doi/10.1145/1352322.1352245
Repenning AIoannidou A(2008)Broadening participation through scalable game designACM SIGCSE Bulletin10.1145/1352322.135224240:1(305-309)Online publication date: 12-Mar-2008
https://dl.acm.org/doi/10.1145/1352322.1352242
Sung KPanitz MWallace SAnderson RNordlinger J(2008)Game-themed programming assignmentsACM SIGCSE Bulletin10.1145/1352322.135224140:1(300-304)Online publication date: 12-Mar-2008
https://dl.acm.org/doi/10.1145/1352322.1352241
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents