I like this[1] introduction by Henk Barendregt (author of the de facto standard work on lambda calculus) [1] http://www.cs.ru.nl/~herman/onderwijs/provingwithC

I like this[1] introduction by Henk Barendregt (author of the de facto standard work on lambda calculus) [1] http://www.cs.ru.nl/~herman/onderwijs/provingwithCA/lambda-sel.pdf http://www.cs.ru.nl/~herman/onderwijs/provingwithCA/lambda-s...