## Abstract

We present the definition of the logical framework TF, the Type Framework.

TF is a lambda-free logical framework; it does not include lambda-abstraction

or product kinds. We give formal proofs of several results in the metatheory of

TF, and show how it can be conservatively embedded in the logical framework

LF: its judgements can be seen as the judgements of LF that are in beta-normal,

eta-long normal form. We show how several properties, such as the injectivity

of constants and the strong normalisation of an object theory, can be proven

more easily in TF, and then ‘lifted’ to LF.

TF is a lambda-free logical framework; it does not include lambda-abstraction

or product kinds. We give formal proofs of several results in the metatheory of

TF, and show how it can be conservatively embedded in the logical framework

LF: its judgements can be seen as the judgements of LF that are in beta-normal,

eta-long normal form. We show how several properties, such as the injectivity

of constants and the strong normalisation of an object theory, can be proven

more easily in TF, and then ‘lifted’ to LF.

Original language | English |
---|---|

Journal | Annals of Pure and Applied Logic |

Publication status | Accepted/In press - 2011 |

## Keywords

- logical framework
- type theory
- canonical logical framework