Neil D. Jones, Carsten K. Gomard, Peter Sestoft. Partial Evaluation for the Lambda Calculus. In John Hatcliff, Torben Æ. Mogensen, Peter Thiemann, editors, Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998. Volume 1706 of Lecture Notes in Computer Science, pages 203-220, Springer, 1998. [doi]
This paper (essentially [12, Chapter 8]) describes partial evaluation for the lambda calculus, augmented with an explicit fixed-point operator. The techniques used here diverge from those used in [12, Chapters 4, 5] and [11] in that they are not based on specialization of named program points. The algorithm essentially leaves some operators (applications, lambdas, etc.) untouched and reduces others as standard evaluation would do it. This simple scheme is able to handle programs that rely heavily on higher-order facilities. The requirements on binding-time analysis are formulated via a type system and an efficient binding-time analysis via constraint solving is outlined. The partial evaluator is proven correct. Chapter 8 from Partial Evaluation and Automatic Program Generation, Prentice-Hall International, 1993, ISBN 0-13-020249-5 (pbk). Reprinted with permission from Pentice-Hall International. All references to “book” in this article refers to this book.