May 26, 2018
Meta-logical framework for deductive systems
The Twelf implementation comprises
- the LF logical framework, including type reconstruction;
- the Elf constraint logic programming language;
- an inductive meta-theorem prover for LF;
- and an Emacs interface.
Twelf provides a uniform meta-language for specifying, implementing, and proving properties of programming languages and logics. Example suites include Cartesian Closed Categories and lambda-calculus, the Church-Rosser theorem for the untyped lambda-calculus, Mini-ML including type preservation and compilation, cut elimination, theory of logic programming, and Hilbert’s deduction theorem.
– the Twelf home page