Twelf is an implementation of the logical frameworkLF developed byFrank Pfenning and Carsten Schürmann atCarnegie Mellon University.[1] It is used forlogic programming and for the formalization ofprogramming language theory.
At its simplest, a Twelf program (called a "signature") is a collection of declarations oftype families (relations) and constants that inhabit those type families. For example, the following is the standard definition of the natural numbers, withz standing for zero ands the successor operator.
nat:type.z:nat.s:nat->nat.
Herenat is a type, andz ands are constant terms. As adependently typed system, types can be indexed by terms, which allows the definition of more interesting type families. Here is a definition of addition:
plus:nat->nat->nat->type.plus_zero:{M:nat}plusMzM.plus_succ:{M:nat}{N:nat}{P:nat}plusM(sN)(sP)<-plusMNP.
The type familyplus is read as a relation between three natural numbersM,N andP, such thatM + N = P. We then give the constants that define the relation: the constantplus_zero indicates thatM + 0 = M. The quantifier{M:nat} can be read as "for allM of typenat".
The constantplus_succ defines the case for when the second argument is the successor of some other numberN (seepattern matching). The result is the successor ofP, whereP is the sum ofM andN. Thisrecursive call is made via the subgoalplus 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 constantplus_succ ("when given a term of typeplus M N P, return a term of typeplus 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 signatures can be executed via a search procedure. Its core is more sophisticated thanProlog, 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 performingI/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 generalizesHorn clauses tohereditary Harrop formulas, which allow for logically well-founded operational notions of fresh-name generation and scoped extension of the clause database.
Twelf is mainly used today as a system for formalizing mathematics, especially the metatheory ofprogramming languages. As such, it is closely related toCoq andIsabelle/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's built-in notion of binding and substitution facilitates the encoding of programming languages and logics, most of which make use of binding and substitution, which can often be directly encoded throughhigher-order abstract syntax (HOAS), where the meta-language's binders represent the object-level binders. Thus standard theorems such as type-preserving substitution andalpha 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 forStandard ML,[2] a foundationaltyped assembly language system from CMU,[3] and a foundationalproof carrying code system from Princeton.
Twelf is written in Standard ML, and binaries are available for Linux and Windows. As of 2006[update], it is under active development, mostly at Carnegie Mellon University.[needs update]
ML programming | ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Software |
|  | ||||||||||||
| Community |
| |||||||||||||
 Book Category:Family:MLCategory:Family:OCamlCategory:Software:OCaml | ||||||||||||||