The Twelf Programming Language (mirror of SVN repository)
Standard ML Emacs Lisp Shell Vim script JavaScript PHP Other
Switch branches/tags
Nothing to show
Latest commit 35216e7 Aug 19, 2013 @robsimmons robsimmons Transfer Mlton build over to mlb files, as they've been asking us to …
…do for years and now insist on.
Permalink
Failed to load latest commit information.
DISTRIBUTE Hold steady on version number, fix the OSX controller to throw libgmp… Mar 8, 2011
TEST Transfer Mlton build over to mlb files, as they've been asking us to … Aug 19, 2013
bin Add LICENSE, BSD-for-real at last Mar 2, 2011
build Transfer Mlton build over to mlb files, as they've been asking us to … Aug 19, 2013
doc fixed duplicated lines in twelf.texi noted by todd wilson Mar 31, 2004
emacs changed some fonts, works better now with Aquamacs Jul 6, 2011
examples-clp *** empty log message *** Mar 8, 2006
examples-delphin Merged Version with tomega checked in Aug 25, 2003
examples Added Ashley-Rollman, Crary, and Harper's solution Nov 14, 2008
exercises *** empty log message *** May 24, 1999
src Exclude unifying outputs in coverage checker. Aug 14, 2013
tex added TeX-style printing Jan 26, 1999
tools Check in partial Twelf wiki code Sep 1, 2010
vim Update vim/syntax/twelf.vim Dec 22, 2012
.cvsignore reconstructed .cvsignore Apr 18, 2002
HISTORY created version 1.4 Dec 28, 2002
LICENSE Mention libgmp in LICENSE Mar 8, 2011
Makefile Transfer Mlton build over to mlb files, as they've been asking us to … Aug 19, 2013
README Improve README slightly, bump version number. Mar 17, 2011
TODO changes to world and mode checker Mar 26, 2001
delphin.cm Merged Version with tomega checked in Aug 25, 2003
delphin.sml Merged Version with tomega checked in Aug 25, 2003
server.cm Touch; need to force a commit to test something Sep 28, 2011
sources.cm automatic style checking disabled Nov 30, 2004

README

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