Kaustuv Chaudhuri
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.
Consult the full list of examples for more details.
Abella uses a two-level logic approach to reasoning. Specifications are made in the logic of second-order hereditary Harrop formulas using lambda-tree syntax. This logic is executable and is a subset of the λProlog language (see the Teyjus system for an implementation of this language). The reasoning logic of Abella is the culmination of a series of extensions to proof theory for the treatment of definitions, lambda-tree syntax, and generic judgments. The reasoning logic of Abella is able to encode the sema
Kaustuv Chaudhuri