Lambda-Free Logical Frameworks
Logic in Computer Science
2008-11-18 v2
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 adequacy theorems for object theories and the injectivity of constants, can be proven more easily in TF, and then `lifted' to LF.
Cite
@article{arxiv.0804.1879,
title = {Lambda-Free Logical Frameworks},
author = {Robin Adams},
journal= {arXiv preprint arXiv:0804.1879},
year = {2008}
}
Comments
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 APAL