View source for Twelf

'''Twelf''' is an implementation of the logical framework [[LF (logical framework)|LF]] developed by [[Frank Pfenning]] and Carsten Schürmann at [[Carnegie Mellon University]].<ref>{{cite conference
 | first = Frank
 | last = Pfenning
 | author2 = Carsten Schürmann
 | title = System description: Twelf - a meta-logical framework for deductive systems
 | conference = Proceedings of the 16th International Conference on Automated Deduction (CADE-16)
 | date = July 1999
 | url = https://www.cs.cmu.edu/~fp/papers/cade99.pdf
 | accessdate = 2019-05-08
 }}</ref> It is used for [[logic programming]] and for the formalization of [[programming language theory]].

==Introduction==
{{further|LF (logical framework)}}

At its simplest, a Twelf program (called a "signature") is a collection of declarations of [[type family|type families]] (relations) and constants that inhabit those type families. For example, the following is the standard definition of the natural numbers, with {{code|z}} standing for zero and {{code|s}} the successor operator.

<syntaxhighlight lang="haskell">
nat : type.

z : nat.
s : nat -> nat.
</syntaxhighlight>

Here {{code|nat}} is a type, and {{code|z}} and {{code|s}} are constant terms. As a [[dependent type|dependently typed]] system, types can be indexed by terms, which allows the definition of more interesting type families. Here is a definition of addition:

<syntaxhighlight lang="haskell">
plus : nat -> nat -> nat -> type.

plus_zero : {M:nat} plus M z M.

plus_succ : {M:nat} {N:nat} {P:nat}
            plus M (s N) (s P)
         <- plus M N P.
</syntaxhighlight>

The type family {{code|plus}} is read as a relation between three natural numbers {{code|M}}, {{code|N}} and {{code|P}}, such that {{code|<nowiki>M + N = P</nowiki>}}. We then give the constants that define the relation: the constant {{code|plus_zero}} indicates that {{code|<nowiki>M + 0 = M</nowiki>}}. The quantifier {{code| {M:nat} }} can be read as "for all {{code|M}} of type {{code|nat}}".

The constant {{code|plus_succ}} defines the case for when the second argument is the successor of some other number {{code|N}} (see [[pattern matching]]). The result is the successor of {{code|P}}, where {{code|P}} is the sum of {{code|M}} and {{code|N}}. This [[Recursion (computer science)|recursive]] call is made via the subgoal {{code|plus M N P}}, introduced with {{code|<-}}. The arrow can be understood operationally as Prolog's {{code|:-}}, 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 {{code|plus_succ}} ("when given a term of type {{code|plus M N P}}, return a term of type {{code|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 {{code| {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.
<!-- to-do: example that is higher order -->
<!-- to-do: concept of canonical forms -->

==Uses==
===Logic programming===
Twelf signatures can be executed via a search procedure. 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 [[input/output|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 clause]]s to [[Harrop formula#Hereditary Harrop formulae and logic programming|hereditary Harrop formulas]], which allow for logically well-founded operational notions of fresh-name generation and scoped extension of the clause database.
<!-- theorem prover?? -->

===Formalizing mathematics===
Twelf is mainly used today as a system for formalizing mathematics, especially the metatheory of [[programming language]]s. As such, it is closely related to [[Coq (software)|Coq]] and [[Isabelle theorem prover|Isabelle]]/[[HOL theorem prover|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 through [[higher-order abstract syntax]] (HOAS), where the meta-language's binders represent the object-level binders. Thus standard theorems such as type-preserving substitution and [[Lambda calculus#α-conversion|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 [[Standard ML]],<ref>{{cite conference
 | first = Daniel
 | last = Lee
 | author2 = Karl Crary
 | author3 = [[Robert Harper (computer scientist)|Robert Harper]]
 | title = Towards a Mechanized Metatheory of Standard ML
 | conference = Proceedings of the 2007 Symposium on the [[POPL|Principles of Programming Languages]]
 | date = January 2007
 | location = [[Nice]], France
 | url = https://www.cs.cmu.edu/~dklee/papers/tslf-popl.pdf
 | accessdate = 2007-02-08
 }}</ref> a foundational [[typed assembly language]] system from CMU,<ref>{{cite conference
 | first = Karl
 | last = Crary
 | title = Toward a Foundational Typed Assembly Language
 | conference = Proceedings of the 2003 Symposium on the [[POPL|Principles of Programming Languages]]
 | year = 2003
 | accessdate = 2007-02-08
 | url = https://www.cs.cmu.edu/~crary/papers/2003/talt/talt.pdf
}}</ref> and a foundational [[proof carrying code]] system from Princeton.

==Implementation==
<!-- to-do: history: ELF -->

Twelf is written in Standard ML, and binaries are available for Linux and Windows. {{asof|2006}}, it is under active development, mostly at Carnegie Mellon University.{{Needs update|date=August 2024}}

== See also ==
*  [[List of proof assistants]]

== References ==
{{Reflist}}
<!-- to-do: references, esp "a framework for defining logics" -->

==External links==
* {{Official website|twelf.org}}, Wiki

{{ML programming}}

[[Category:Dependently typed languages]]
[[Category:Logic programming languages]]
[[Category:Theorem proving software systems]]
[[Category:Type theory]]
[[Category:Logic in computer science]]