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.
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.
The current version 1.4 from December 27, 2002 incorporates the following major changes from Twelf 1.3 from September 13, 2000.
%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.
%total. The former can also be used to check that sets of patterns in the arguments of a type family are exhaustive.
%tabled a(to declare a type family to be tabled) and
%querytabledto start tabled search.
Assuming you are running on a Unix system with SML of New Jersey 110.0.3
already installed (see section 14 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
% 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 %
Go to the first, previous, next, last section, table of contents.