The Fox Project
Logical Frameworks

Contents Recent Talks | Recent Publications | Software | Collaborations | Further Links
Elsewhere Bibliography | Twelf Implementation

A logical framework is a meta-language for the formalization of logics and programming languages. Most of the research at CMU on logical frameworks is centered around LF and its implementation in the Twelf system.

The technology of logical frameworks is used in the Fox project in two major ways:

  • In the proof-carrying code architecture, formal proofs for the safety of binaries are expressed in LF and attached to the code as checkable certificates. This uses a specialized theorem prover that generates proof objects and an optimized checker for verifying their validity.
  • In our language design efforts we use the logical framework to specify, prototype, and experiment with our languages. Recently, we have been able to also formally reason about some properties of type systems and operational semantic specifications.

Current research on logical frameworks in the context of the Fox project at CMU is concentrating on design and implementation of a module system, space-efficient representation and time-efficient checking of proof terms, and improvements to the theorem proving and meta-reasoning capabilities of the Twelf system.

Overview references:

Recent Talks

Three Applications of Strictness in the Efficient Implementation of Higher-Order Terms
Frank Pfenning.
Workshop on Implementations of Logic, Réunion, France, November 2000.
Slides, Related paper
Language Techniques for Provably Safe Mobile Code
Frank Pfenning.
Distinguished lecture, Computing and Information Sciences, Kansas State University, October 2000.
Slides, Related paper

Recent Publications

Below are some recent papers related to logical frameworks in the Fox project. A more complete bibliography is also available.

Logical Frameworks
Frank Pfenning.
Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov, editors, Chapter 16, Elsevier Science and MIT Press. In preparation.
Available here until publication (PDF, PostScript, Twelf code).
On Equivalence and Canonical Forms in the LF Type Theory
Robert Harper and Frank Pfenning.
Technical Report CMU-CS-00-148, July 2000. An extended abstract appeared at the Workshop on Logical Frameworks and Meta-Languages (LFM'99), Paris, France, September 1999.
Termination and Reduction Checking in the Logical Framework
Brigitte Pientka and Frank Pfenning.
Workshop on Automation of Proofs by Mathematical Induction, Pittsburgh, Pennsylvania, June 2000.
Automated Techniques for Provable Safe Mobile Code
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning.
Theoretical Computer Science, To appear in a special issue on Dependable Computing. Preliminary version appeared in the proceedings of the DARPA Information Survivability Conference and Exposition (DISCEX 2000), vol 1, pages 406-419, Hilton Head Island, South Carolina, January 2000.


The Fox project has created two main software artifacts related to logical frameworks.

  • Twelf is an implementation of LF, a constraint logic programming interpretation of LF, and an experimental automated theorem prover. The current official release is Twelf 1.2. Twelf 1.3 is available as a beta release. Sources and binaries for various architectures, User's Guide, example suites, tutorials, and other information are available for download from the Twelf home page.
  • The Touchstone implementation of the Proof-Carrying Code architecture contains a proof-generating theorem prover and an efficient checker for proofs represented in a fragment of LF. It is available upon request.


  • Secure Internet Programming, a project at Princeton University under the direction of Edward Felten and Andrew Appel is using the Twelf implementation of LF for proof-carrying code, proof-carrying authentication, and related applications.
  • The Stanford Validity Checker is currently updated to generate proof objects that are checkable in the Twelf system. Contact Aaron Stump for more information.
  • Carsten Schürmann at Yale University is actively working on the Twelf system and applying it for certification of intermediate code.

Further Links

  • The Twelf home page, including sources and binaries of the Twelf system, documentation, examples, and further related information.
  • Computation and Deduction, a set of course notes explaining the LF logical framework, its methodology, and its implementation.
  • The home page on logical frameworks, including pointers to other systems, researchers, and a bibliography.

[ Home | Contact Information | Publications | Researchers ]
[ FoxNet | Typed Intermediate Languages | Proof-Carrying Code ]
[ Logical Frameworks | Staged Computation | Language Design ]