7 lines
349 B
Text
7 lines
349 B
Text
|
Abella is an interactive theorem prover based on lambda-tree syntax. This means
|
||
|
|
that Abella is well-suited for reasoning about the meta-theory of programming
|
||
|
|
languages and other logical systems which manipulate objects with binding. For
|
||
|
|
example, the following applications are included in the distribution of Abella.
|
||
|
|
|
||
|
|
WWW: http://abella-prover.org/
|