Logical framework
In type theory, the LF logical framework is a popular example of framework for describing and experimenting with logics. Other famous logical frameworks include calculus of constructions and NuPRL. The key features of the LF type theory are:
- based on a three-level higher-order dependently typed lambda calculus
- decidable and efficient type checking
- 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 prover