Abella Tutorial: Reasoning about Computational Systems using Abella

Preparation

Abella can be used in two modes: online and offline.

Online

1. Go to /tutorial/try with a modern Web Browser.
2. Make sure JavaScript is enabled.
3. There is nothing to install or configure! Abella will run completely inside your Browser.

Offline

You will need to have a working OCaml toolchain, preferably managed with the help of OPAM. Follow these steps to install Abella:

1. Run the command opam install abella to install Abella in `opam config var bin` (which should be in your $PATH).
2. Optional but recommended: If you want ProofGeneral support for Abella, then:
   1. Download and install ProofGeneral. Abella is only compatible with development versions with version numbers beginning with 4.3pre.
   2. Navigate to your ProofGeneral installation.
   3. Create a subdirectory abella from the topmost directory of the ProofGeneral installation.
   4. Copy the files `opam config var share`/abella/emacs/pg/*.el to that abella directory.
   5. Run M-x customize-variable proof-assistant-table from within Emacs and add the entry (abella "Abela" "thm") to the list.
      If this variable is not customizable, you need to make sure that ProofGeneral/generic is in your load-path and then eval (require 'proof-site).
   6. Restart Emacs.

Content

• Slides (PDF) from the presentation

Links

• Abella: A System for Reasoning about Relational Specifications (PDF) by D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, and Y. Wang. Journal of Formalized Reasoning, v. 7(2). 2014
• Specifying and Reasoning About Computational Systems (PDF) by G. Nadathur. Lecture notes for a graduate course.
• Programming with Higher-Order Logic by D. Miller and G. Nadathur. Cambridge University Press. 2012.