
Twelf

Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory.
Introduction.
At its simplest, a Twelf program (called a "signature") is a collection of declarations of type families and constants that inhabit those type families. For example, the following is the standard definition of the natural numbers, with codice_1 standing for zero and codice_2 the successor operator.
 nat : type.
 z : nat.
 s : nat -> nat.
Here codice_3 is a type, and codice_1 and codice_2 are constant terms. As a dependently typed system, types can be indexed by terms, which allows the definition of more interesting type families (relations). Here is a definition of addition:
 plus : nat -> nat -> nat -> type.
 plus_zero : {M:nat} plus M z M.
 plus M (s N) (s P)
 <- plus M N P.
The type family codice_6 is read as a relation between three natural numbers codice_7, codice_8 and codice_9, such that M + N = P. We then give the constants that define the relation: codice_10 indicates that any natural number codice_7 plus zero is still codice_7. The quantifier codice_13 can be read as "for all codice_7 of type codice_3".
The constant codice_16 defines the case for when the second argument is the successor of some other number codice_8 (see pattern matching). The result is the successor of codice_9, where codice_9 is the sum of codice_7 and codice_8. This recursive call is made via the subgoal codice_22, introduced with codice_23. The arrow can be understood operationally as Prolog's codice_24, or as logical implication ("if M + N = P, then M + (s N) = (s P)"), or most faithfully to the type theory, as the type of the constant codice_16 ("when given a term of type codice_22, return a term of type codice_27").
Twelf features type reconstruction and supports implicit parameters, so in practice one usually does not need to explicitly write codice_13 (etc.) above.
These simple examples do not display LF's higher-order features, nor any of its theorem checking capabilities. See the Twelf distribution for its included examples.
Uses.
Twelf is used in several different ways.
Logic programming.
Twelf signatures can be executed via a search procedure, so Twelf can be used as a logic programming language. Its core is more sophisticated than Prolog, since it is higher-order and dependently typed, but it is restricted to pure operators: there is no cut or other extralogical operators (such as ones for performing I/O) as are often found in Prolog implementations, which may make it less well-suited for practical logic programming applications. Some uses of Prolog's cut rule can be obtained by declaring that certain operators belong to deterministic type families, which avoids recalculation. Also, like λProlog, Twelf generalizes Horn clauses to hereditary Harrop formulas, which allow for logically well-founded operational notions of fresh-name generation and scoped extension of the clause database.
Formalizing mathematics.
Twelf is mainly used today as a system for formalizing mathematics (especially the metatheory of programming languages). As such, it is closely related to Coq and Isabelle/HOL/HOL Light. However, unlike those systems, Twelf proofs are typically developed by hand. Despite this, for the problem domains at which it excels, Twelf proofs are often shorter and easier to develop than in the automated, general-purpose systems.
Twelf is particularly well suited to the encoding of programming languages and logics, because it has a built-in notion of binding and substitution. Most logics and programming languages of interest make use of binding and substitution. When implemented in Twelf, binders can often be directly encoded using the technique of higher-order abstract syntax (HOAS), in which the meta-language (Twelf) binders are used to represent the object-level binders. As a consequence, standard theorems such as type-preserving substitution and alpha conversion come "for free".
Twelf has been used to formalize many different logics and programming languages (examples are included with the distribution). Among the larger projects are a proof of safety for the Standard ML programming language, a foundational typed assembly language system from CMU, and a foundational proof carrying code system from Princeton.
Implementation.
Twelf is written in Standard ML and binaries are available for Linux and Microsoft Windows. it is under active development (mostly at Carnegie Mellon University).