Classification of Typed/Untyped Lambda Calculi Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi?
I'm particularly looking for statements of their expressive power, equivalences to logic/arithmetic systems or computation methods, and analogies to programming languages if applicable.
While I certainly intend to read, something like a reference table outlining the calculi and their equivalences/differences/place in the hierarchy would be a HUGE reference for helping me sort them out.
Not saying the below is correct, just trying to sketch together some of the impressions i have to see if they at least serve as a starting point (or something to correct!)

Untyped lambda calculus - eq. to first order logic - cannot do X
Simply typed lambda calculus - eq to ... logic, related to Lisp?
'Polymorphic' lambda calc -
etc.
Calculus of Constructions - intutionist logic?
Combinatory Logic - comparable to ??? typed lambda calculus, related to APL/J kind of languages

If this ties into the lambda cube and its three axes all the better.
While I'm familiar with the basics of lambda calculus and programming with functional languages, I have never wrapped my head around, or made any significant connections to, the type systems involved and different flavors of lambda (and maybe pi?) calculi.
When I attempt to research this i cant help but find myself sidetracked, opening up many browser tabs and branching in so many directions I never get into any of them with any depth!
I'm not sure if what I'm asking for is reasonable, but hopefully at the very least I've painted enough of a picture to suggest some reading that can explain what im looking for?
Your table is a bit confused; here's a better one.


Untyped lambda calculus -- no logical interpretation, as Andrej notes
Simply typed lambda calculus -- intuitionistic propositional logic
Polymorphic lambda calculus -- pure second-order logic (ie, without first-order quantifiers)
Dependent types -- generalization of first-order logic
Calculus of constructions -- generalization of higher-order logic


Type dependency is more general than first-order quantification, since it turns proofs into objects you can quantify over. Lambda calculi corresponding to ordinary intuitionistic FOL exist, but are not widely used enough to have a special name -- people tend to go straight to dependent types.

You can also relate the syntactic form of a calculus to logical systems, as well.


Combinator calculi (eg, SKI combinators) -- Hilbert-style systems
A-normal form -- sequent calculus 
Ordinary typed lambda calculus -- natural deduction