./lang/twelf, Meta-language for proving properties of languages and logics

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]


Branch: pkgsrc-2011Q4, Version: 1.4nb1, Package name: twelf-1.4nb1, Maintainer: richards+netbsd

From http://www.twelf.org, heavily edited:

Twelf is a research project concerned with the design,
implementation, and application of logical frameworks. It
provides a uniform meta-language for specifying, implementing, and
proving properties of programming languages and logics.

Example suites include Cartesian Closed Categories and
lambda-calculus, the Church-Rosser theorem for the untyped
lambda-calculus, Mini-ML including type preservation and
compilation, cut elimination, theory of logic programming, and
Hilbert's deduction theorem.

The principal authors of Twelf are Frank Pfenning and Carsten
Schuermann, with major contrubtions by Brigitte Pientka, Roberto
Virga, and Kevin Watkins.


Required to run:
[editors/emacs] [lang/smlnj]

Master sites:

SHA1: 3476fc18b7d0596df2c9847102d239de3eae813b
RMD160: 31ca91650fe46fb9dbe785eef91234c6c4d2d120
Filesize: 1428.865 KB

Version history: (Expand)