The Call-by-Need Lambda Calculus

Zena M. Ariola; Matthias Felleisen; John Maraist; Martin Odersky; Philip Wadler

doi:10.1145/199448.199507

The Call-by-Need Lambda Calculus

Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, Philip Wadler

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.

Original language	English
Title of host publication	POPL '95 Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Publisher	ACM
Pages	233-246
Number of pages	14
ISBN (Print)	0-89791-692-1
DOIs	https://doi.org/10.1145/199448.199507
Publication status	Published - 1995

Access to Document

10.1145/199448.199507

http://dl.acm.org/citation.cfm?doid=199448.199507

Cite this

@inproceedings{e4dd694b0ad44834918832ab232f2c8c,

title = "The Call-by-Need Lambda Calculus",

abstract = "The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.",

author = "Ariola, {Zena M.} and Matthias Felleisen and John Maraist and Martin Odersky and Philip Wadler",

year = "1995",

doi = "10.1145/199448.199507",

language = "English",

isbn = "0-89791-692-1",

pages = "233--246",

booktitle = "POPL '95 Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages",

publisher = "ACM",

}

TY - GEN

T1 - The Call-by-Need Lambda Calculus

AU - Ariola, Zena M.

AU - Felleisen, Matthias

AU - Maraist, John

AU - Odersky, Martin

AU - Wadler, Philip

PY - 1995

Y1 - 1995

N2 - The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.

AB - The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.

U2 - 10.1145/199448.199507

DO - 10.1145/199448.199507

M3 - Conference contribution

SN - 0-89791-692-1

SP - 233

EP - 246

BT - POPL '95 Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

PB - ACM

ER -

The Call-by-Need Lambda Calculus

Abstract / Description of output

Access to Document

Fingerprint

Cite this