2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/174219We 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 adequacy theorems for object theories and the injectivity of constants, can be proven more easily in TF, and then `lifted' to LF.v2: Mistakes were found in several proofs in v1. Several results have been weakened. v3: Minor mistakes corrected and line lengths fixed. This version submitted to APALLogic in Computer ScienceF.4.1; F.4.3text