Computer Science – Logic in Computer Science
Scientific paper
2008-04-11
Computer Science
Logic in Computer Science
v2: Mistakes were found in several proofs in v1. Several results have been weakened. v3: Minor mistakes corrected and line len
Scientific paper
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.
No associations
LandOfFree
Lambda-Free Logical Frameworks does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Lambda-Free Logical Frameworks, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Lambda-Free Logical Frameworks will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-706826