All Projects → standardml → Twelf

standardml / Twelf

Licence: other
The Twelf Programming Language (mirror of SVN repository)

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

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].