LF (logical framework)

From Free net encyclopedia

In type theory, the LF logical framework was one of the first logical frameworks, that is a formal calculus for the description of formal systems and reasoning about them. Three key features of the LF type theory are:

• It is based on a three-level higher-order dependently typed lambda calculus
• It has a decidable and efficient type checking algorithm
• It supports natural encodings of logics in terms of higher-order abstract syntax

The LF logical framework is implemented in 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 proverTemplate:Comp-sci-stub