A great bootstrap into the world of Lambda Calculus (LC). Every concept is clearly explained, proofs are detailed in every step, and notation properly introduced before use. The material goes from a formal introduction of LC, reduction (alpha, beta), Church-Rosser, LC and primitive recursion to typed LC. A couple of pages are spent on extensions and reduction systems. Exercises are present without solution, some are simple application others require some creativity.