Release of Twelf 1.2 Logical Framework
We are proud to announce the first release of Twelf (Version 1.2). The
the LF logical framework, including type reconstruction;
the Elf constraint logic programming language;
a meta-theorem prover for LF (very preliminary);
and an Emacs interface.
The principal authors of Twelf are
Frank Pfenning and
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.
It also includes a complete User's Guide and example suite; a tutorial
is available from the Twelf homepage. Twelf is written in Standard ML
and uses an inference engine based on explicit substitutions. Twelf
has been developed at Carnegie Mellon University and runs under SML/NJ
and MLWorks on various Unix platforms and Windows 95/98/NT.
We maintain a firstname.lastname@example.org, a low-volume moderated mailing list
for announcements regarding Elf and its implementation in Twelf. Please
send requests to email@example.com.