Twelf
Copyright (C) 1997-2011, Frank Pfenning and Carsten Schuermann
Authors: Frank Pfenning
Carsten Schuermann
With contributions by:
Brigitte Pientka
Roberto Virga
Kevin Watkins
Jason Reed
Twelf is an implementation of
- the LF logical framework, including type reconstruction
- the Elf constraint logic programming language
- a meta-theorem prover for LF (very preliminary)
- a set of expansion modules to deal natively with numbers and strings
- an Emacs interface
Installing
==========
For complete installation instructions, see http://twelf.org/
Twelf can be compiled and installed under Unix, either as a separate
"Twelf Server" intended primarily as an inferior process to Emacs, or as
a structure Twelf embedded in Standard ML.
To build with SML of New Jersey type "make smlnj." To build with MLton type
"make mlton." If you are building Twelf through SML of New Jersey, you may need
to run "make buildid" first.
Files
=====
README --- this file
Makefile --- enables make
server.cm --- used to build Twelf Server
sources.cm --- used to build Twelf SML
bin/ --- utility scripts, heaps, binaries
build/ --- build files (type "make" to see options)
doc/ --- (Outdated) Twelf user's guide
emacs/ --- Emacs interface for Twelf
examples/ --- various case studies
examples-clp/ --- examples of use of the numbers and strings extensions
src/ --- the SML sources for Twelf
tex/ --- TeX macros and style files
vim/ --- Vim interface for Twelf