Lambda the Ultimate

I am trying to figure out the relation of equational logic to ordinary Haskell evaluations (not type level or anything exotic).
I posted similar question here and on the Haskell-cafe, which provided some very good insights. This lead me to the lambda calculus and even more questions.
Here is my take ...
Lambda calculus is generally considered as a formal model (is this in the model theoretic sense?) of computation. But is it a logic?

First what is a Logic?
Hunter [1] says a formal system consist of
a) Well formed formula (WFF)
b) Axioms
c) A model, which is an interpretation of the WFF
d) Rules of inference, independent of model
Which are all determined by fiat by the language creator.
Of course these pieces must all work in harmony. I guess it is the rules of inference (d) that make it a logic. See [2] for a deep look at this question

Hankin[3] puts lambda calculus in the context of general formal systems, consisting of;
a) Notation, a set of terms (WFF)
b) Theories or set axioms relating terms,Hankin[3] provides a theory for LC (seems very close to the axioms of equational logic).
c) Models that give mathematical meaning, in LC this is usually functions over sets
Hankin[3] goes on to describe reduction. I am aware that logics can be encoded in LC and reductions would be inferences (but logics can be encoded in Java).

So, it seems that lambda calculus is a formal system, but is it a logic?
If it is not what is its relation with logic?

[1]Metalogic: An Introduction to the Metatheory of Standard First-Order Logic,Geoffrey Hunter, University of California Press, 1971
http://en.wikipedia.org/wiki/Metalogic
[2] What is a logic, Mossakowski et al. http://cseweb.ucsd.edu/~goguen/pps/nel05.pdf
[3] An Introduction to Lambda Calculi for Computer Scientists, 2nd edition 2004, Chris Hankin

Sure this topic has been around before,
This post is to refresh contemporary ideas, i.e. circa 2010.

-- Justin Johansson