Twelf
   HOME

TheInfoList



OR:

Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at
Carnegie Mellon University Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania. One of its predecessors was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools; it became the Carnegie Institute of Technology ...
. It is used for
logic programming Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
and for the formalization of
programming language theory Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is clos ...
.


Introduction

At its simplest, a Twelf program (called a "signature") is a collection of declarations of type families (relations) and constants that inhabit those type families. For example, the following is the standard definition of the natural numbers, with standing for zero and the successor operator. nat : type. z : nat. s : nat -> nat. Here is a type, and and are constant terms. As a dependently 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 : plus M z M. plus_succ : plus M (s N) (s P) <- plus M N P. The type family is read as a relation between three natural numbers , and , such that . We then give the constants that define the relation: the constant indicates that . The quantifier can be read as "for all of type ". The constant defines the case for when the second argument is the successor of some other number (see
pattern matching In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually has to be exact: "either it will or will not be ...
). The result is the successor of , where is the sum of and . This recursive call is made via the subgoal , 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 ("when given a term of type , return a term of type "). Twelf features type reconstruction and supports implicit parameters, so in practice, one usually does not need to explicitly write (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. Its core is more sophisticated than
Prolog Prolog is a logic programming language associated with artificial intelligence and computational linguistics. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
, 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 λProlog, also written lambda Prolog, is a logic programming language featuring polymorphic typing, modular programming, and higher-order programming. These extensions to Prolog are derived from the higher-order hereditary Harrop formulas u ...
, 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 language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...
s. As such, it is closely related to Coq and
Isabelle Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of ''Elizabeth (given name), Elisabeth'' (ultimately Hebrew ''Elisheba, Elisheva''), Arising in ...
/
HOL Hol is a municipality in Viken county, Norway. Administrative history The area of Hol was separated from the municipality Ål in 1877 to become a separate municipality. In 1937 a part of neighboring Uvdal with 220 inhabitants moved to Hol munic ...
/
HOL Light HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations. HOL Light is ...
. 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 In computer science, higher-order abstract syntax (abbreviated HOAS) is a technique for the representation of abstract syntax trees for languages with variable binders. Relation to first-order abstract syntax An abstract syntax is ''abstract'' b ...
(HOAS), where the meta-language's binders represent the object-level binders. Thus 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
Standard ML Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of ...
, a foundational
typed assembly language In computer science, a typed assembly language (TAL) is an assembly language that is extended to include a method of annotating the datatype of each value that is manipulated by the code. These annotations can then be used by a program (type check ...
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 Windows. , it is under active development, mostly at Carnegie Mellon University.


See also

* List of proof assistants


References

{{Reflist


External links


Twelf Project wiki
Dependently typed languages Logic programming languages Theorem proving software systems Type theory Logic in computer science