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