LF (logical framework)
From Free net encyclopedia
(Difference between revisions)
| Revision as of 22:44, 18 January 2006 Jon Awbrey (Talk | contribs) indent lists ← Previous diff |
Current revision Jon Awbrey (Talk | contribs) indent lists |
Current revision
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