Commentary by cpressey on Lambda Calculus works
The Calculi of Lambda-Conversion
Introduction to Combinators and the Lambda Calculus
Barendregt 1984 should be on this list but isn't. So, this is.
A Short Introduction to the Lambda Calculus
A fixed-point combinator can be given (the Y combinator), but in the simply-typed lambda calculus, it cannot be given a type. Thus recursion cannot be done in the STLC and thus the STLC is not Turing-complete.
Introduction to Lambda Calculus
This is where I found out about Combinatory Reduction Systems from.
Chapter 5: The Untyped Lambda Calculus
Untyped Lambda Calculus
A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure
So one thing I haven't wrapped my head around here, is that this lambda calculus has abstractions that take a list of parameters, instead of one abstraction each; which is a lot more like a conventional programming language (with functions but no currying by default). And this is isomorphic to the sequent calculus? Does this mean anything?
The Lambda Calculus is Algebraic
"Yes, but what IS an indeterminate?"
A Lambda Calculus with Naive Substitution
This paper is cited in something else I read -- possibly "Equational Logic as a Programming Language".
I have read this paper, although maybe I missed the point when I did.
Basically, the substitution operator substitutes using a list of positions, rather than a name? This seems underwhelming.
A Graph-like Lambda Calculus for which Leftmost-Outermost Reduction is Optimal
I read this, but not entirely comprehendingly -- I could stand to read it again.
This paper is cited in "Equational Logic as a Programming Language".
Staples gives top-level rules for beta-reduction of the lambda calculus (after it has been converted to de Bruijn indexes) which are essentially algebraic-looking, and which resemble the S, K, I combinators:
(\x.x G) -> G
(\x.y G) -> y (where y =/= x)
(\x.(E F) G) -> ((\x.E G) (\x.F G))
(\x.\y.E G) -> (\y.(\x E G))
Which seems to imply that you can derive the S, K, I combinators from analyzing the lambda calculus algebraically.
Which seems weird, because I thought the S, K, I combinators came originally from (Schoenfinkel) taking that basic axiom system of Hilbert's and making them "point-free".
But weirder things have happened. So, OK.
On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control
For a long time it has been widely thought that a classical proof, as opposed to an intuitionistic one, did not carry any computational content... but! Types-as-propositions.
I guess by "Syntactic Theory of Sequential Control" they refer to continuations.