Description

Extensibella is an interactive proof assistant for proving properties about extensible languages built by independently-developed modules which may build on each other. Module writers prove properties for each module independently, as they were written, with a guarantee the proofs can be combined to form a proof for any composed language built by combining some number of modules. These properties may be introduced by any module.

Extensibella proves properties using induction and case analysis on judgments. In some situations, depending on where the property is introduced relative to where the relevant judgment and syntactic category for the case analysis are introduced, the cases may be distributed across the modules so each module proves the cases it introduces. However, there are some situations where a module must prove a property will hold for other modules it does not know. In any situation, a proof in Extensibella guarantees the property will hold for any composed language.

For more information on our view of extensible languages, see this document. For information on how our modular reasoning works, see this document.

Download

There are two ways to get Extensibella:

• Download the tarball. This includes a pre-compiled copy of Extensibella, so all that is needed is extracting the archive and running ./install.
• Clone the GitHub repository and build it using the build script, then the install script. Building will require installing the Silver attribute grammar system first. Extensibella can also be built from the downloaded tarball.

Running Extensibella also requires installing the Abella proof assistant.

Extensibella has been tested only on Linux, but may run on Mac OS or on the Windows Subsystem for Linux (WSL) if Abella can be installed. No operating systems have been tested to be ruled out.

Documentation

• A walkthrough on the structure of modular metatheory and proving properties demonstrating the use of Extensibella for modular metatheory
• The Extensibella reference guide has a brief description of Extensibella's syntax and tactics.
• A list of theorems in the Extensibella standard library is available to aid in developing proofs.
• Further examples are available.

Sterling for Language Specifications

Currently, the only system for specifying languages for reasoning in Extensibella is Sterling. Sterling defines languages via modules describing syntax and semantics using inference rules using the same notion of extensible languages as Extensibella exists.

About the Name

Extensibella reasons about extensible languages using Abella to check the validity of the logical reasoning apart from the restrictions specific to extensibility. The name "Extensibella" is a combination of extensible and Abella, where each word gave a little to make the combination work.