Classics
I was surprised to find that these classic papers are available online:
- Alonzo church, "A Set of Postulates for the Foundation of Logic." 1932 (The original lambda-caculus paper.)
- Alonzo Church, "An Unsolvable Problem of Elementary Number Theory." 1936
- Moses Schönfinkel, "Über die Bausteine der mathematischen Logik." 1924. (In German.)
- Nikolas de Bruijn, "Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem." 1972.
- Alonzo Church and J. B. Rosser, "Some properties of conversion." 1936.
It's interesting to read Church's papers to see how he's approaching the project. Initially, he's trying to clarify the notion of a free variable in logic, or rather to chuck it out in favor of a clear discipline for binding variables. Because he's looking at foundational issues in logic, he's at great pains to identify his assumptions.
A minor historical fact: alpha- and beta-conversion are defined in these early Church papers, but not with those names; they're identified as I-conversion and II-conversion (there is a conversion rule III, which looks like the reverse of beta-conversion).