Lambda-Free Logical Frameworks

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.