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