blob: 912d5264ab27576c3915f0bfe5759db9ec799765 (
plain) (
tree)
|
|
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/
|