Another good reference, that also introduces some PLT notation, is Loh 2001, "Introduction to the Dependently-Typed Lambda Calculus" [1], as well as the textbook by Pierce [2], which has a formally-verified spiritual successor [3].
Types and Programming Languages by Pierce is an amazing book. I'm still far from finishing it, but if anyone is looking for a good introduction to the field, this is it. I consider it to be kind of like the SICP of PL. :)
Edit: Ah, and the Software Foundations books are amazing. I did a little course on formal verification during 2020 and learned a ton. Now every time I work with some kind of type system, I feel frustrated that I can't express everything that I want to in my type system.
Programming Languages Foundations is an excellent book. Of course it assumes familiarity with Coq (which Logical Foundations covers). Formal proofs about PLs are often boring and tedious to carry out on paper, especially if the property they're stating is clearly obvious, so doing them in an interactive theorem prover is a win-win for checking your work and making the concepts more palatable.
Not covered in this PDF but extremely important is the notion of substitution. This is the only computational operation of the lambda calculus, and is the reason why lambda calculus is Turing-complete. Substitution is also hard to get right, but here's how it would work with "fresh" variables[0]. Alternatively one may avoid names altogether and use de Bruijn indices[1], however there's a significant performance cost in doing so. See λ-calculus cooked four ways[2] for more information.
What's a good way for someone without much of a background in maths to start grokking this? I've had had several encounters with the lambda calculus over the years (including a coworker who is absolutely in love with it), but it's never really clicked for me in any meaningful way.
It starts with the general rules of lambda calculus, then build up some basic functions (like in the PDF linked in this thread) and continues to build data types like Natural Numbers, List, String, Tree and operators for manipulating them. The book also explains about the evaluation methods as well as covering how ML and LISP uses lambda calculus.
For someone fluent in Python, David Beazley gives a brilliant introduction to lambda calculus here: https://www.youtube.com/watch?v=pkCLMl0e_0k This is great fun to follow through on a rainy afternoon!
[1] http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/index....