Go to the first, previous, next, last section, table of contents.

1 Introduction

Twelf is the current version of a succession of implementations of the logical framework LF. Previous systems include Elf (which provided type reconstruction and the operational semantics reimplemented in Twelf) and MLF (which implemented module-level constructs loosely based on the signatures and functors of ML still missing from Twelf).

Twelf should be understood as research software. This means comments, suggestions, and bug reports are extremely welcome, but there are no guarantees regarding response times. The same remark applies to these notes which constitute the only documentation on the present Twelf implementation.

For current information including download instructions, publications, and mailing list, see the Twelf home page at http://www.cs.cmu.edu/~twelf/. This User's Guide is published as

 Frank Pfenning and Carsten Schuermann
 Twelf User's Guide
 Technical Report CMU-CS-98-173, Department of Computer Science, 
 Carnegie Mellon University, November 1998.

Below we state the typographic conventions in this manual.

for Twelf or ML code
for characters and small code fragments
for placeholders in code
for input in verbatim examples
for keystrokes
for mathematical expressions
for emphasized phrases

File names for examples given in this guide are relative to the main directory of the Twelf installation. For example `examples/guide/nd.elf' may be found in
`/usr/local/twelf/examples/guide/nd.elf' if Twelf was installed into the `/usr/local/' directory.

1.1 New Features

While the underlying type theory has not changed, the Twelf implementation differs from older Elf implementation in a few ways. Mostly, these are simplifications and improvements. The main feature which has not yet been ported is the Elf server interface to Emacs. Also, while the type checker is more efficient now, the operational semantics does not yet incorporate some of the optimizations of the older Elf implementations and is therefore slower.

Syntax (see section 3 Syntax)
The quote `'' character is no longer a special character in the lexer, and `=' (equality) is now a reserved identifier. The syntax of %name declarations has changed by allowing only one preferred name to be specified. Also, %name, %infix, %prefix and %postfix declarations must be terminated by a period `.' which previously was optional. Further, single lines comments now must start with `%whitespace' or `%%' in order to avoid misspelled keywords of the form `%keyword' to be ignored.
Type theory
Elf 1.5 had two experimental features which are not available in Twelf: polymorphism and the classification of type as a type.
Definitions (see section 3.3 Definitions)
Twelf offers definitions which were not available in Elf.
Searching for definitions (see section 5.2 Solve Declaration)
Elf had a special top-level query form sigma [x:A] B which searched for a solution M : A and then solved the result of subsituting M for x in B. In Twelf this mechanism has been replaced by a declaration %solve c : A which searches for a solution M : A and then defines c = M : A, where the remaining free variables are implicitly universally quantified.
Query declarations (see section 5.1 Query Declaration)
Twelf allows queries in ordinary Elf files as `%query' declarations. Queries are specified with an expected number of solutions, and the number of solutions to search for, which can be used to test implementations.
Operational semantics (see section 5.5 Operational Semantics)
Twelf eliminates the distinction between static and dynamic signatures. Instead, dependent function types {x:A} B where x occurs in the normal form of B are treated statically, while non-dependent function type A -> B or B <- A or {x:A} B where x does not occur in B are treated dynamically.
Modes (see section 6 Modes)
Twelf offers a mode checker which was only partially supported in Elf.
Termination (see section 7 Termination)
Twelf offers a termination checker which can verify that certain programs represent decision procedures.
Theorem prover (see section 8 Theorem Prover)
Although very limited at present, an experimental prover for theorems and meta-theorems (that is, properties of signatures) is now available. It does not yet support lemmas or meta-hypothetical reasoning, which are currently under development.
Emacs interface (see section 11 Emacs Interface)
The Elf mode has remained basically unchanged, but the Elf server interface has not yet been ported.

1.2 Quick Start

Assuming you are running on a Unix system with SML of New Jersey already installed (see section 12 Installation) you can build Twelf as follows. Here `%' is assumed to be the shell prompt. You may need to edit the file `Makefile' to give the proper location for sml-cm.

% gunzip twelf-1-2.tar.gz
% tar -xf twelf-1-2.tar
% cd twelf
% make
% bin/twelf-server
Twelf 1.2, Aug 27 1998
%% OK %%

You can now load the examples used in this guide and pose an example query as shown below. The prompt from the Twelf top-level is `?-'. To drop from the Twelf top-level to the ML top-level, type C-c (CTRL c). To exit the Twelf server you may issue the quit command or type C-d (CTRL c).

Config.read examples/guide/sources.cfg
?- of (lam [x] x) T.
T = arrow T1 T1.
More? y
No more solutions
?- C-c
%% OK %%

Go to the first, previous, next, last section, table of contents.