Lambda-Free Logical Frameworks

Adams, Robin

(2011)

Adams, Robin (2011) Lambda-Free Logical Frameworks. Annals of Pure and Applied Logic

Our Full Text Deposits

Full text access: Open

Full text file - 330.23 KB

Links to Copies of this Item Held Elsewhere


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 the injectivity of constants and the strong normalisation of an object theory, can be proven more easily in TF, and then ‘lifted’ to LF.

Information about this Version

This is a Accepted version
This version's date is: 2011
This item is not peer reviewed

Link to this Version

https://repository.royalholloway.ac.uk/items/f6d98574-c4dd-fa35-69a9-49980f3c2cd6/5/

Item TypeJournal Article
TitleLambda-Free Logical Frameworks
AuthorsAdams, Robin
Uncontrolled Keywordslogical framework, type theory, canonical logical framework
DepartmentsFaculty of Science\Computer Science

Identifiers

Deposited by Research Information System (atira) on 14-Jun-2012 in Royal Holloway Research Online.Last modified on 14-Jun-2012


Details