Abella 2.1.0-dev

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 the unreleased development version 2.1.0-dev, pinned at commit 6b5bc46. The documentation for the released 2.0.8 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 fragment of λProlog 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.

Development highlights

The development version adds reasoning-level modules in .thmod files and inline in .thm files, the Axiom command, the compute and fchain tactics, computation guards declared with Suspend, and a no-argument form of clear. The command-line tools also accept .thmod sources, and the prover can check stratification strictly.

Where to go next

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