Lambda-Free Logical Frameworks. / Adams, Robin.

In: Annals of Pure and Applied Logic, 2011.

Research output: Contribution to journalArticle

Forthcoming

Documents

  • Lfree18

    Submitted manuscript, 322 KB, PDF-document

Links

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.
Original languageEnglish
JournalAnnals of Pure and Applied Logic
Publication statusAccepted/In press - 2011
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 1891982