Lambda-Free Logical Frameworks

Robin Adams

Research output: Contribution to journalArticlepeer-review

102 Downloads (Pure)


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.
Original languageEnglish
JournalAnnals of Pure and Applied Logic
Publication statusAccepted/In press - 2011


  • logical framework
  • type theory
  • canonical logical framework

Cite this