CMU-CS-98-173
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-98-173

Twelf User's Guide
Version 1.2

Frank Pfenning, Carsten Schurmann

November 1998

CMU-CS-98-173.ps
CMU-CS-98-173.pdf
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 http://www.cs.cmu.edu/~twelf.

80 pages


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

This page maintained by reports@cs.cmu.edu