Learning Lambda Calculus

Question

What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus?

Specifically, I am interested in the following areas:

• Untyped lambda calculus
• Simply-typed lambda calculus
• Other typed lambda calculi
• Church's Theory of Types (I'm not sure where this fits in).

(As I understand, this should provide a solid basis for the understanding of type theory.)

Any advice and suggestions would be appreciated.

Answer 1

It might be nice to work through Structure and Interpretation of Computer Programs, which is available online for free. This book is an introduction to computer science and the programming language Scheme, which is a flavor of the programming language Lisp, which is based on the lambda calculus. Although it is not strictly a book about the lambda calculus, it might be fun or useful to gain some hands-on and "practical" experience with the lambda calculus by reading some of this book and working through some of its exercises.

Answer 2

Recommendations:

1. Barendregt & Barendsen, 1998, Introduction to lambda-calculus;
2. Girard, Lafont & Taylor, 1987, Proofs and Types;
3. Sørenson & Urzyczyn, 1999, Lectures on the Curry-Howard Isomorphism.

All of these are mentioned in the LtU Getting Started thread.

Answer 3

I like Type Theory and Functional Programming by Simon Thompson.

Answer 4

Alligator Eggs is a cool way to learn lambda calculus.

Also learning functional programming languages like Scheme, Haskell etc. will be added fun.

Answer 5

Here are a couple of resources that will get you started:

1. The Lambda Calculus, Its Syntax and Semantics - This is a must!

2. Lecture Notes on the Lambda Calculus by Peter Selinger

3. History of Lambda Calculi

4. Impact of Lambda Calculus on Logic and Computer Science

5. Introduction to Lambda Calculus

6. Lambda Calculi with Types

7. Tutorial Introduction to Lambda Calculus

8. Call-by-name, call-by-value and the Lambda Calculus

9. Control operators, the SECD-machine, and
   the lambda-calculus. - With effects

10. Modified basic functionality in combinatory logic- H.B. Curry.

11. The principal type scheme of an object in combinatory logic. - J. Roger Hindley.

Since I am a computer science graduate, most of these are geared towards computer scientists rather than logicians.

Bonus : There is a new book that has come out Semantics Engineering with PLT Redex. I haven't read it but people have told me good things about it.

I hope this helps. Please feel free to ask me any questions. Thanks.

Answer 6

Lambda-Calculus and Combinators, an Introduction by J. ROGER HINDLEY and JONATHAN P. SELDIN is a great (and relatively modern) resource that doesn't assume any previous knowledge.

It is available online here.