diff options
| author | edwin <edwin@FreeBSD.org> | 2005-11-26 20:49:47 +0800 |
|---|---|---|
| committer | edwin <edwin@FreeBSD.org> | 2005-11-26 20:49:47 +0800 |
| commit | e694ffd61ab89e0fbc1364c4e220d310fdbf138c (patch) | |
| tree | 7ef71dd7a9096fa08e3389761d2f6b82ba3b4917 /lang/twelf/pkg-descr | |
| parent | c90aea498c9dd1dc0c6ba4c32064ca9402f0d924 (diff) | |
| download | freebsd-ports-gnome-e694ffd61ab89e0fbc1364c4e220d310fdbf138c.tar.gz freebsd-ports-gnome-e694ffd61ab89e0fbc1364c4e220d310fdbf138c.tar.zst freebsd-ports-gnome-e694ffd61ab89e0fbc1364c4e220d310fdbf138c.zip | |
New port: lang/twelf A meta-logical framework for deductive systems
The Twelf implementation comprises
* the LF logical framework, including type reconstruction;
* the Elf constraint logic programming language;
* an inductive meta-theorem prover for LF;
* and an Emacs interface.
PR: ports/84625
Submitted by: "Andrew Bernard" <andrew@hobnob.com>
Diffstat (limited to 'lang/twelf/pkg-descr')
| -rw-r--r-- | lang/twelf/pkg-descr | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/lang/twelf/pkg-descr b/lang/twelf/pkg-descr new file mode 100644 index 000000000000..f32f99997930 --- /dev/null +++ b/lang/twelf/pkg-descr @@ -0,0 +1,19 @@ + +The Twelf implementation comprises + + * the LF logical framework, including type reconstruction; + * the Elf constraint logic programming language; + * an inductive meta-theorem prover for LF; + * and an Emacs interface. + +Twelf 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 Twelf home page + +WWW: http://www.cs.cmu.edu/~twelf |