About The Twelf Project
STELF 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 STELF 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 STELF are
with major contributions by
- Brigitte Pientka,
- Roberto Virga, and
- Kevin Watkins
STELF 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.