Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 The Twelf Project
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);
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.
Re-packaged on March 8 in a form suitable for SML/NJ 110.0.07,
SML/NJ 110.53, Poly/ML 4.1.3 and MLton 20040227
We have made a working version of Twelf 1.5 (Dec 3, 2004)
available. It fixes a significant bug in the totality checker of Twelf
1.4 which let some false meta-theorems pass.
It contains several undocumented features, among them
some uniqueness checking and improved tabling.
The current alpha release of Twelf is version 1.4, Dec 27, 2002.
World checker
Coverage checker
Totality checker
Deterministic search
Portability (SML/NJ, Poly/ML, and MLton are supported)
Family-level definitions (preliminary)
Tabled search (preliminary)
Software
The current stable release of Twelf is Version 1.2. The current alpha
release is Version 1.4. Twelf is written in Standard ML and uses an
inference engine based on explicit substitutions. Twelf has been tested
under SML/NJ,
Poly/ML, and
MLton on various Unix platforms and
Windows 95/98/NT.
Source distribution can be compiled with SML/NJ, Poly/ML and MLton under
Linux, Windows, and MacOS X. This is first version of Twelf whose
source is fully compatible with the SML'97 Definition.
Twelf 1.4 has several new features including world checking, coverage
checking, totality checking, tracing type reconstruction, and
use of definitions during proof search (see
New Features).
Working Version 1.3R4 (obsolete) twelf-1-3R4.tar.gz (1.4 MB)
for Linux/Unix/Solaris, including User's Guide and example
suites. Requires SML'97 (preferably SML of NJ, version 110 or higher).
See the README-1-3R4 file for further
information.
1.3 alpha (obsolete) twelf-1-3.tar.gz (1.1 MB)
for Linux/Unix/Solaris, including User's Guide and example
suites. Requires SML'97 (preferably SML of NJ, version 110 or higher).
See the README-1-3 file for further
information. A binary distribution for x86/Linux
(twelf-1-3-0.i386.rpm, 1.4 MB)
is also available.
1.3 alpha (obsolete) twelf-1-3.exe (5.7 MB) for Windows
9x/ME/NT/2000. This includes binaries, sources, User's Guide,
and examples suites. See the README-1-3
file for further information.
twelf-1-2.tar.gz (717KB,
README-1-2), includes User's Guide and example
suites. Requires SML'97 (preferably SML of NJ, version 110 or higher).
It has been tested under Linux, SunOS, Sun/Solaris and Windows
95/98/NT.
twelf-1-2-1.i386.rpm (959KB,
README), a precompiled rpm file for
RedHat Linux, includes User's Guide and example suites but no source
code.
twelf-1-2.exe (1,868KB,
README), a precompiled version for Windows
95/98/NT, includes User's Guide and example suites but no source
code.
Logical Frameworks---A Brief Introduction,
lecture noes from the Marktoberdorf Summer School, July 2001. Appeared
in Proof and System Reliability, pp 137-166, H. Schwichtenberg
and R. Steinbrüggen, eds, Kluwer Academic Publishers, 2002.
(PDF)
Logical Frameworks (209 KB compressed, also available in PDF), article for the Handbook of
Automated Reasoning, Alan Robinson and Andrei Voronkov, editors,
Chapter 17, pp. 1063-1147, Elsevier Science and MIT Press.
Note: The course notes provide a tutorial introduction to
LF and Elf, although at present some material in Chapter 4 is out of
date with respect to the current implementation.
Recent Publications and Drafts
Below is an update and excerpt of the bibliography on LF and Elf. These are the most
recent papers directly relevant to the Twelf implementation.
Frank Pfenning and Carsten Schürmann.
System description: Twelf - a meta-logical framework for deductive
systems.
In H. Ganzinger, editor, Proceedings of the 16th International
Conference on Automated Deduction (CADE-16), pages 202-206, Trento, Italy,
July 1999. Springer-Verlag LNAI 1632.
Available in PostScript format.
Frank Pfenning.
Computation and Deduction.
Cambridge University Press, 2000.
In preparation. Draft from April 1997 available electronically.
Available in PostScript format.
Frank Pfenning and Carsten Schürmann.
Algorithms for equality and unification in the presence of notational
definitions.
In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types
for Proofs and Programs. Springer-Verlag LNCS 1657, 1998.
To appear.
Available in PostScript format.
Frank Pfenning and Carsten Schürmann.
Twelf User's Guide, 1.2 edition, September 1998.
Available as Technical Report CMU-CS-98-173, Carnegie Mellon
University.
Below are other recent publications relevant to research on logical
frameworks in the Twelf project.
Andrew W. Appel and Edward W. Felten.
Proof-carrying authentication.
In G. Tsudik, editor, Proceedings of the 6th Conference on
Computer and Communications Security, Singapore, November 1999. ACM Press.
To appear.
Iliano Cervesato.
Proof-theoretic foundation of compilation in logic programming
languages.
In J. Jaffar, editor, Proceedings of the 1998 Joint
International Conference and Symposium on Logic Programming (JICSLP'98),
pages 115-129, Manchester, UK, June 1998. MIT Press.
Available in PostScript format.
Iliano Cervesato and Frank Pfenning.
A linear logical framework.
Information and Computation, 1998.
To appear in a special issue with invited papers from LICS'96, E.
Clarke, editor.
Available in PostScript format.
Robert Harper and Frank Pfenning.
On equivalence and canonical forms in the LF type theory.
In A. Felty, editor, Proceedings of the Workshop on Logical
Frameworks and Meta-Languages (LFM'99), Paris, France, September 1999.
To appear.
Available in PostScript format.
Alberto Momigliano and Frank Pfenning.
The relative complement problem for higher-order patterns.
In D. De Schreye, editor, Proceedings of the International
Conference on Logic Programming (ICLP'99), Las Cruces, New Mexico, November
1999. MIT Press.
To appear.
Available in PostScript format.
Alberto Momigliano.
Elimination of negation in a logical framework.
2000. Draft.
Available in PostScript format.
Frank Pfenning.
Reasoning about deductions in linear logic.
In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction
(CADE-15), pages 1-2, Lindau, Germany, July 1998. Springer-Verlag LNCS
1421.
Abstract for invited talk.
Available in PostScript format.
Mark Plesko and Frank Pfenning.
A formalization of the proof-carrying code architecture in a linear
logical framework.
In A. Pnueli and P. Traverso, editors, Proceedings of the
Workshop on Run-Time Result Verification, Trento, Italy, July 1999.
Available electronically.
Jeff Polakow and Frank Pfenning.
Ordered linear logic programming.
Technical Report CMU-CS-98-183, Department of Computer Science,
Carnegie Mellon University, December 1998.
Available electronically.
Jeff Polakow and Frank Pfenning.
Natural deduction for intuitionistic non-commutative linear logic.
In J.-Y. Girard, editor, Proceedings of the 4th International
Conference on Typed Lambda Calculi and Applications (TLCA'99), pages
295-309, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581.
Available in PostScript format.
Jeff Polakow and Frank Pfenning.
Relating natural deduction and sequent calculus for intuitionistic
non-commutative linear logic.
In Andre Scedrov and Achim Jung, editors, Proceedings of the
15th Conference on Mathematical Foundations of Programming Semantics, New
Orleans, Louisiana, April 1999.
Electronic Notes in Theoretical Computer Science, Volume 20.
Available in PostScript format.
Carsten Schürmann and Frank Pfenning.
Automated theorem proving in a simple meta-logic for LF.
In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction
(CADE-15), pages 286-300, Lindau, Germany, July 1998. Springer-Verlag LNCS
1421.
Available in PostScript format.
Aaron Stump and David L. Dill.
Generating proofs from a decision procedure.
In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC
Workshop on Run-Time Result Verification, Trento, Italy, July 1999.
Roberto Virga.
Higher-Order Rewriting with Dependent Types.
PhD thesis, Department of Mathematical Sciences, Carnegie Mellon
University, 1999.
Forthcoming.
Researchers on Logical Frameworks at Carnegie Mellon
Faculty, graduate students, and undergraduate students currently involved
in research on logical frameworks at Carnegie Mellon University:
We maintain two mailing lists for the Twelf project through
mailman. The moderated mailing list which is used for announcments
related to Twelf is called twelf-list. The other is called
twelf-developer. It serves as discussion forum for people who
are working on the Twelf implementation.