Twelf User’s Guide

Version 1.4

Frank Pfenning and Carsten Schuermann

Copyright © 1998, 2000, 2002 Frank Pfenning and Carsten Schuermann


[ << ] [ < ] [ Up ] [ > ] [ >> ]         [Top] [Contents] [Index] [ ? ]

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.

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


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated on July 9, 2016 using texi2html 5.0.