Twelf

Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.

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 z standing for zero and s the successor operator.

Here nat is a type, and z and s 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:

The type family plus is read as a relation between three natural numbers M, N and P, such that M + N = P. We then give the constants that define the relation: plus_zero indicates that any natural number M plus zero is still M. The quantifier {M:nat} can be read as "for all M of type nat".

The constant plus_succ defines the case for when the second argument is the successor of some other number N (see pattern matching). The result is the successor of P, where P is the sum of M and N. This recursive call is made via the subgoal plus M N P, introduced with <-. The arrow can be understood operationally as Prolog's :-, 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 plus_succ ("when given a term of type plus M N P, return a term of type plus M (s N) (s P)").

Twelf features type reconstruction and supports implicit parameters, so in practice one usually does not need to explicitly write {M:nat} (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.

Twelf is used in several different ways.

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 of the use of cut rule as used in Prolog is obtained through the ability to declare that certain operators belong to deterministic type families, which avoids recalculation. Also, like λProlog, Twelf generalizes the Horn clauses underlying Prolog to hereditary Harrop formulas, which allow for logically well-founded operational notions of fresh-name generation and scoped extension of the clause database.

...
Wikipedia