| |
The Fox Project
Logical Frameworks
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:
-
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
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.
- 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
]
Fox_Project@cs.cmu.edu
http://www.cs.cmu.edu/~fox/
|