LF is the abbreviation commonly used for the Edinburgh Logical Framework presented by Harper, Honsell, and Plotkin in A Framework for Defining Logics. Harper, Honsell, and Plotkin introduce both LF, which is a dependently typed lambda-calculus, and a systematic methodology for representing deductive systems, such as programming languages and logics, in this lambda-calculus. This methodology is often called the judgments as types principle, because a judgment in a deductive system is represented as an LF type family classifiying (the representations of) derivations of the judgement. Derivations in a deductive system can be checked by type checking their LF representations. An LF representation is adequate iff it is isomorphic to the original description of the deductive system.
- an implementation of the LF logical framework, which can be used to type check LF representations
- a logic programming language based on LF
- a metatheorem checker, which can be used to verify proofs of theorems about LF representations
- Read the Introductions to Twelf to learn more about LF and Twelf.
- Canonical forms: describes the modern way of thinking about the LF type theory.
- Higher-order abstract syntax
- Judgments as types
- Higher-order judgements
- Bibliography of LF
- LF (logical framework) on Wikipedia
Robert Harper, Furio Honsell, Gordon Plotkin - A framework for defining logics
- J. ACM 40(1):143--184, New York, NY, USA,1993
- BibtexAuthor : Robert Harper, Furio Honsell, Gordon Plotkin
Title : A framework for defining logics
In : J. ACM -
Address : New York, NY, USA
Date : 1993
This page is incomplete. We should expand it.