LF

From The Twelf Project

LF is the abbreviation commonly used for the Edinburgh Logical Framework presented by Harper, Honsell, and Plotkin in A Framework for Defining Logics^[1]. 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.

Twelf includes:

• 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

[edit] See also

• 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

[edit] References

1. ↑ Robert Harper, Furio Honsell, Gordon Plotkin - A framework for defining logics
   

   J. ACM 40(1):143--184, New York, NY, USA, 1993

   Bibtex

   Auteur : Robert Harper, Furio Honsell, Gordon Plotkin
   Titre : A framework for defining logics
   Dans : J. ACM -
   Adresse : New York, NY, USA
   Date : 1993