I would like to program an interpreter for the original, untyped lambda calculus. Where can I find a single, complete, and authoritative source on the lambda calculus, including an unambiguous specification of the rules for reducing lambda calculus forms?
I have found plenty of good resources for learning about the lambda calculus, but there seem to be various subtle gotchas, particularly with regard to variable capture, as well as different ways of reducing forms, e.g. with regard to order of evaluation, and I'm never sure if I've found a source that is both complete and correct in its description of the lambda calculus.
Chapter 1 of Lectures on the Curry-Howard Isomorphism - Morten Heine B. Sørensen, Pawel Urzyczyn