blob: df5296b3b088d286c3b5f4b82e6fcf7178a46541 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
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
|
