Abella 2.0.8

Abella is an interactive theorem prover based on λ-tree syntax (also known as higher-order abstract syntax, HOAS). It is designed for reasoning about formal systems specified using judgments in a two-level logic.

This is the documentation for Abella 2.0.8, specifically the 2.0.8.3 release. The documentation for the unreleased development version is available from the version selector in the navigation bar.

Install Abella, then start with the walkthrough for an introduction, or read the advanced walkthrough after that. The reference and tools sections cover the command language and the command-line programs.

The two-level logic

Abella separates the specification of an object system from the reasoning about it:

• The specification logic is a λProlog-like logic in which inference rules are written directly as clauses. A specification is stored in a .sig signature and a .mod module.
• The reasoning logic is used to state and prove properties of the relations defined by the specification. Proofs are recorded in .thm files.

Both logics are simply typed, and both support lambda-tree syntax for representing binding. This makes it possible to model capture-avoiding substitution, freshness, and renaming without encoding variables as numbers or strings.

Where to go next

• Installation
• Walkthrough: subject reduction
• Advanced walkthrough: type uniqueness
• File structure
• Top-level declarations
• Specification logic
• Reasoning logic
• Schematic polymorphism
• Command reference
• Tactics reference
• Tools
• Examples
• Changelog