Computer Science Department
School of Computer Science, Carnegie Mellon University


Twelf User's Guide
Version 1.2

Frank Pfenning, Carsten Schurmann

November 1998
Twelf Software

Keywords: Logical frameworks, logic programming, automated deduction

This user's guide describes the current version of a succession of implementations of the logical framework LF. It documents the syntax, term reconstruction, and operational semantics already available in an earlier implementation called Elf. The new features described here include a mode checker, a termination checker, an experimental theorem prover for verifying properties of Elf programs, and an Emacs interface.

The software itself is available through the Twelf home page at

80 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by