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).

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.

<UL> <LI> <A HREF="http://www.cs.cmu.edu/~twelf/">Twelf Home Page</A> </LI> </UL>

Below we state the typographic conventions in this manual.

code

for Twelf or ML code

`samp'

for characters and small code fragments

metavar

for placeholders in code

keyboard

for input in verbatim examples

key

for keystrokes

math

for mathematical expressions

emph

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

The current version 1.6 from March 29, 2009 incorporates the following major changes from Twelf 1.3 from September 13, 2000.

World Checking (see section Regular Worlds).

World checking verifies regularity of the parameters and hypothesis that can be introduced by terms in a signature. The new declarations are %block and %worlds. This formally checks part of the adequacy theorem that is usually left implicit in the encoding and is is used centrally by the coverage checker.

Coverage and Totality Checking (see section Coverage, see section Totality).

Proofs of meta-theorems given in relational form can now be verified if they are of order 2 or less. The new relevant declarations are %covers and %total. The former can also be used to check that sets of patterns in the arguments of a type family are exhaustive.

Mode Checking (see section Modes)

Mode checking has been extended so that multiple modes can be checked for the same predicate, even though not simultaneously. This allows certain relations to serve as proofs for biconditional meta-theorems. Also, some predicates in constraint domains can have multiple modes simultaneously in effect.

Tabled Search (see section Tabled Logic Programming)

An experimental logic programming engine for tabled logic programming is available in this release. The corresponding declarations are %tabled a (to declare a type family to be tabled) and %querytabled to start tabled search.

Deterministic Search (see section Deterministic Type Families)

Type families can be declared deterministic for search, which means that after the first solution has been found, backtracking will not find any further solutions. The relevant declaration is %deterministic a.

Family-Level Definitions (see section Clause Definitions)

Twelf now permits family-level definitions that are opaque to logic programming execution. However, not all aspects of the present release handle them properly, so they should be considered an experimental feature. Furthermore, defined constants will now be used for logic programming search when prefixed with %clause.

Tracing Term Reconstruction (see section Tracing Reconstruction)

Term reconstruction can print each typing judgment it establishes in order to help diagnose subtle type errors or ambiguities.

Portability (see section Installation)

Twelf has been ported to be compliant with the Definition of Standard ML in its 1997 revision. As a result, it now supports Poly/ML and MLton in addition to Standard ML of New Jersey (SML/NJ).

Module System (see section Module System)

A module system featuring signature, structure, and view declarations has been added. The module system is conservative in the sense that a modular signature is internally elaborated into a non-modular one. However, the modular structure is remembered to allow for module level reasoning.

1.2 Quick Start

Assuming you are running on a Unix system with SML of New Jersey 110.0.3 already installed (see section 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.

% gunzip twelf-1-4.tar.gz
% tar -xf twelf-1-4.tar
% cd twelf
% make
% bin/twelf-server
Twelf 1.4, Dec 27 2002
%% OK %%

For SML/NJ version 110.20 or greater, use make -f smlnj/Makefile. For Poly/ML use make -f polyml/Makefile. For MLton use make -f mlton/Makefile.

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).

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

This document was generated by Florian Rabe on April, 3 2009 using texi2html 1.76.