From The Twelf Project
Jump to: navigation, search

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

See also


  1. Robert Harper, Furio Honsell, Gordon Plotkin - A framework for defining logics
    J. ACM 40(1):143--184, New York, NY, USA,1993
    Author : 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.