Theory mainly concerned with $\lambda$-calculus? Automata theory is mainly concerned with Turing machines and all its relatives-in-spirit. $\lambda$-calculus is rather rarely mentioned in textbooks on automata theory.
What's the common name of the theory mainly concerned with $\lambda$-calculus and its relatives? (I think, "mathematical logic", "computability theory", "programming language theory" and "recursion theory" are too general, compared to "automata theory". But there should be an "$\lambda$-theory", shouldn't it?)
 A: In recent years almost anything I have read about lambda calculus has been about typed lambda calculus. Broadly speaking, I think computer scientists would say that these papers were part of the field known as Type Theory.
If that doesn't quite fit what you want I'd suggest reading the PLT article on Wikipedia.
For example, there is a family of lambda calculi that can be arranged in what is known as the lambda cube. The wikipedia article starts "In mathematical logic and type theory..."
A: I don't know of one that seems sufficiently general.  The theory's at an intersection: 


*

*It (in its untyped guise) is one of the four most important Turing-complete computation systems;

*It is algebraically natural, connected fundamentally to Cartesian-closed categories (though with horrid baggage around $\alpha$-equivalence);

*It is a foundational theory, possibly the theory that best captures the notion of schematic function; and

*It plays an important role in philosophical logic, due to its link to natural deduction, which is among the few treatments of formal logic that is relevant to the actuality of how we reason. 


Maybe a name formed out of keywords from several of these domains would give a suitable term?  How about Cartesian function-calculus?
Edited
A: "combinatory logic"
A: Untyped Lambda Calculus is part of the Recursion Theory, I would say. Typed Lambda Calculus is Type Theory, and is connected with constructive mathematics.
The Lambda-Calculus is a concept that can be applied to many parts of mathematics, so there are few books especially about Lambda-Calculus (Imho lambda calculus : logic = measure theory : analysis, sort of). And the ones I know (i.e. Barendregt, etc.) are just referring to it as "Lambda Calculus".
A: The lambda calculus is considered one of the fundamental topics in Theoretical Computer Science. You can study it from many points of view:


*

*If you study its denotational semantics, then you use algebra and category theory.

*If you study its operational semantics, then you mainly use rewriting theory.

*If you study logic, then you will be interested in its type system. You may also be interested in the related system of combinatory logic.

*If you are a functional programmer, then you are using lambda calculus as a Turing-complete formalism.

*If you study the foundations of mathematics, then the lambda calculus is related to many foundational systems: Illative combinatory logic, Map Theory, Type Theory, ...


However the term "lambda-theory" is already reserved for a very specific concept: a lambda-theory is a congruence on the set of lambda-terms that contains alpha-beta conversion.
