Lambda-Free Logical Frameworks

2008/04/11 by Robin Adams, Adams, Robin · 2 citations
Computer Science · #F.4.1 #F.4.3 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · doi:10.48550/arxiv.0804.1879

openalex publication_date 2008/04/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31

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.

Citations

• A framework for defining logics

Cited by

• Dependently Sorted Nominal Signatures
• Compositional Semantics for Probabilistic Programs with Exact Conditioning

Related

• A Logic for Reasoning About LF Specifications
• A Meta-Programming Approach to Realizing Dependently Typed Logic Programming
• Transporting Theorems about Typeability in LF Across Schematically Defined Contexts
• Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search
• A framework for defining logics