Lambda-Free Logical Frameworks
| dc.creator | Adams, Robin | |
| dc.date | 2008-04-11 | |
| dc.date | 2008-11-18 | |
| dc.date.accessioned | 2026-07-07T10:18:32Z | |
| dc.date.available | 2026-07-07T10:18:32Z | |
| dc.description | 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. | |
| dc.description | 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 | |
| dc.identifier | https://arxiv.org/abs/0804.1879 | |
| dc.identifier | http://arxiv.org/abs/0804.1879 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/174219 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.4.1; F.4.3 | |
| dc.title | Lambda-Free Logical Frameworks | |
| dc.type | text |