5 lines
317 B
Plaintext
5 lines
317 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.
|