Logical framework vs type theory
Summary. A logical framework is a meta-language for the formalisation of deductive systems, where deductions become syntactic objects.

Of course what counts as a meta-language is quite vague, and it is helpful to understand the historical development of logical frameworks.
The first logical framework was de Bruijn's Automath (1), which is based on $\lambda$-calculus. Many of the ideas from the Automath language family have found their way into modern logical frameworks. Martin-L&ouml;f's work on constructive type-theories, also based on $\lambda$-calculi, has also been influential.

Edinburgh's LF (2) is a very influential logical framework.
Edinburgh LF is what you get when you enrich the simply typed $\lambda$-calculus with type-dependency. That's all. In order to make type-dependency precise, one needs to replace the function space operator $A \rightarrow B$ on types with type-abstraction, usually written $\Pi x^A. B$, and introduce the kind of types, as well as kind abstraction.
In terms of rules, the key is in the elimiation rule for $A \rightarrow B$, resp. $\Pi x^A. B$:

$$
\newcommand{\TYPES}[3]{#1 \vdash #2 : #3}
\newcommand{\SUBST}[2]{\{#1/#2\}}
\frac{
   \TYPES{\Gamma}{\color{red}{M}}{A \rightarrow B} 
      \qquad
   \TYPES{\Gamma}{\color{red}{N}}{A}  }{
 \TYPES{\Gamma}{\color{red}{MN}}{B}   }
      \qquad
\frac{
   \TYPES{\Gamma}{{\color{red}M}}{\Pi x^A. B} 
      \qquad
   \TYPES{\Gamma}{\color{red}{N}}{A}  }{
 \TYPES{\Gamma}{{\color{red}{MN}}}{B\SUBST{{\color{red}N}}{x}}   }
$$

On the left we have the rule for the simply typed $\lambda$-calculus, on the right the
rule that generalises the left with type dependency. We see that a value 'flows' into the
type in the conclusion on the right.

I think the interactive proof assistant Isabelle uses intuitionistic second order logic based on $\lambda$-calculus, without any numbers or recursive data types as logical framework. Various others have been proposed.

One advantage of using $\lambda$-calculi as logical framework  is that binding constructs like universal quantifiers can be implemented using the framework's $\lambda$-binder. Note that most logical frameworks are expressively weak: the frameworks  support object-level reasoning, but are insufficient to perform much meta-theoretic reasoning beyond the fact that a particular object-level statement is a theorem. In fact the metal-logic is usually so weak that even proving the deduction theorem for a Hilbert-style object logic is impossible. Of course nothing prevents you from using more powerful type-theories as a logical framework.

For these practical and historical reasons, most logical frameworks in use today are typed $\lambda$-calculi, i.e. type-theories. See (3, 4) for more in-depth discussions of logical frameworks.


N. de Bruijn: The Mathematical Language AUTOMATH, Its Usage, and Some of Its Extensions.
R. F. Harper, F. Honsell, G. Plotkin: A Framework for Defining Logics.
F. Pfenning: Logical frameworks.
F. Pfenning: Logical frameworks -- A Brief Introduction.