blob: 912d5264ab27576c3915f0bfe5759db9ec799765 (
plain) (
blame)
1
2
3
4
5
6
|
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/
|
