λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.

Since many people ask how to reduce λ-expressions with the intermediate steps, take a look at Lambda calculus reduction workbench and its interpreter.

Free books and papers

An Introduction To Functional Programming Through Lambda Calculus by Greg Michaelson
Lambda Calculi with Types by Henk Barendregt
Introduction to Lambda Calculus by Henk Barendregt and Erik Barendsen

Interpretation of the Lambda Calculus in Practical Foundations of Mathematics by Paul Taylor
Note: This is an online book as HTML, no downloadable PDF version

history | show excerpt | excerpt history