Logical Framework - LF

LF

In the case of the LF logical framework, the meta-language is the -calculus. This is a system of first-order dependent function types which are related by the propositions as types principle to first-order minimal logic. The key features of the -calculus are that it consists of entities of three levels: objects, types and families of types. It is predicative, all well-typed terms are strongly normalizing and Church-Rosser and the property of being well-typed is decidable. However, type inference is undecidable.

A logic is represented in the LF logical framework by the judgements-as-types representation mechanism. This is inspired by Per Martin-Löf's development of Kant's notion of judgement, in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical and the general, correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A logical system is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements .

An implementation of the LF logical framework is provided by the Twelf system at Carnegie Mellon University. Twelf includes

• a logic programming engine
• meta-theoretic reasoning about logic programs (termination, coverage, etc.)
• an inductive meta-logical theorem prover