Interactive theorem prover

<rendered-html><p>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.</p> </rendered-html>