**Lambda-Free Logical Frameworks.** / Adams, Robin.

Research output: Contribution to journal › Article › peer-review

Forthcoming

**Lambda-Free Logical Frameworks.** / Adams, Robin.

Research output: Contribution to journal › Article › peer-review

Adams, R 2011, 'Lambda-Free Logical Frameworks', *Annals of Pure and Applied Logic*. <http://arxiv.org/abs/0804.1879>

Adams, R. (Accepted/In press). Lambda-Free Logical Frameworks. *Annals of Pure and Applied Logic*. http://arxiv.org/abs/0804.1879

@article{64c25b66149e4ef899e3a0efc20da7e9,

title = "Lambda-Free Logical Frameworks",

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-abstractionor product kinds. We give formal proofs of several results in the metatheory ofTF, and show how it can be conservatively embedded in the logical frameworkLF: 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 injectivityof constants and the strong normalisation of an object theory, can be provenmore easily in TF, and then {\textquoteleft}lifted{\textquoteright} to LF.",

keywords = "logical framework, type theory, canonical logical framework",

author = "Robin Adams",

year = "2011",

language = "English",

journal = "Annals of Pure and Applied Logic",

issn = "0168-0072",

publisher = "Elsevier",

}

TY - JOUR

T1 - Lambda-Free Logical Frameworks

AU - Adams, Robin

PY - 2011

Y1 - 2011

N2 - We present the definition of the logical framework TF, the Type Framework.TF is a lambda-free logical framework; it does not include lambda-abstractionor product kinds. We give formal proofs of several results in the metatheory ofTF, and show how it can be conservatively embedded in the logical frameworkLF: 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 injectivityof constants and the strong normalisation of an object theory, can be provenmore easily in TF, and then ‘lifted’ to LF.

AB - We present the definition of the logical framework TF, the Type Framework.TF is a lambda-free logical framework; it does not include lambda-abstractionor product kinds. We give formal proofs of several results in the metatheory ofTF, and show how it can be conservatively embedded in the logical frameworkLF: 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 injectivityof constants and the strong normalisation of an object theory, can be provenmore easily in TF, and then ‘lifted’ to LF.

KW - logical framework

KW - type theory

KW - canonical logical framework

M3 - Article

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

SN - 0168-0072

ER -