7 lines
349 B
Plaintext
7 lines
349 B
Plaintext
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/
|