Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
What is the difference between logical framework and type theory? Both of them have types, terms, and are based on dependently typed lambda calculus.
We have Edinburg LF which is based on lambda-pi calculus, however, it seems to me that there's some subtle difference there.
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ö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.
