About The Twelf Project
Twelf is a research project concerned with the design, implementation, and application of logical frameworks funded by the National Science Foundation under grants CCR-9619584 and CCR-9988281 Meta-Logical Frameworks, CCR-0306313 Efficient Logical Frameworks (Principal Investigator: Frank Pfenning) and by DARPA under the contract number F196268-95-C-0050 The Fox Project: Advanced Languages for Systems Software (Principal Investigators: Robert Harper, Peter Lee, and Frank Pfenning).
The Twelf implementation comprises
- the LF logical framework, including type reconstruction;
- the Elf constraint logic programming language;
- an inductive meta-theorem prover for LF (very preliminary);
- and an Emacs interface.
The principal authors of Twelf are
with major contrubtions by
- Brigitte Pientka,
- Roberto Virga, and
- Kevin Watkins
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.
