The Call-by-Need Lambda Calculus

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationPOPL '95 Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
PublisherACM
Pages233-246
Number of pages14
ISBN (Print)0-89791-692-1
DOIs
Publication statusPublished - 1995

Fingerprint Dive into the research topics of 'The Call-by-Need Lambda Calculus'. Together they form a unique fingerprint.

Cite this