Source-linked AI summary
The Abella Interactive Theorem Prover (System Description)
Andrew Gacek
TL;DR
Reasoning about object languages with binding requires representations that support structural semantics and proofs about specifications. Abella pairs an executable specification logic using λ-tree syntax with a reasoning logic that embeds it. The paper reports applications including normalization proofs, cut admissibility, and type uniqueness.
Problem
Abella addresses reasoning about object languages presented by recursive syntactic rules, including properties of specifications involving binding.
Source: §3.1 · p. 3Method
Abella encodes object languages in executable second-order hereditary Harrop specifications with λ-tree syntax, then reasons about them in G using specification-aware tactics.
Source: §3 · p. 2, §3.1 · p. 3Results
Abella has been used to prove λ-calculus normalization properties, cut admissibility for a sequent calculus, and type uniqueness for simply typed λ-terms.
Source: §5 · p. 5Takeaways & Limitations
The reported examples include proofs about evaluation, typing, normalization, and cut admissibility using Abella’s treatment of specifications and their meta-properties.
Source: §5 · p. 5G currently supports natural-number induction, while structural induction and coinduction are supported in the implementation but described as features of an extended logic.
Source: §6 · p. 6
Abstract
from arXiv · showhide
Abella is an interactive system for reasoning about aspects of object languages that have been formally presented through recursive rules based on syntactic structure. Abella utilizes a two-level logic approach to specification and reasoning. One level is defined by a specification logic which supports a transparent encoding of structural semantics rules and also enables their execution. The second level, called the reasoning logic, embeds the specification logic and allows the development of proofs of properties about specifications. An important characteristic of both logics is that they exploit the lambda tree syntax approach to treating binding in object languages. Amongst other things, Abella has been used to prove normalizability properties of the lambda calculus, cut admissibility for a sequent calculus and type uniqueness and subject reduction properties. This paper discusses the logical foundations of Abella, outlines the style of theorem proving that it supports and finally describes some of its recent applications.
2 The Logic Underlying Abella
Abella’s reasoning logic G combines higher-order logic, fixed-point definitions, and natural-number induction with λ-tree syntax for representing binding. Its ∇ quantifier and extended definitions support reasoning about generic names, freshness, and dependencies in object-language syntax.
2 The Logic Underlying Abella
- G uses λ-tree syntax to represent object-level binding through meta-level abstraction, building α-equivalence and capture-avoiding substitution into the logic.Object-language encodings therefore need not implement those features themselves.Source: §2 · p. 1
- The ∇ quantifier expresses generic truth, requiring a formula to hold without assumptions about the quantified name, unlike ∀.The paper treats ∇-bound variables using nominal constants that are fresh for the formula and permutable.Source: §2 · pp. 1–2
- G’s fixed-point definitions admit ∇-quantifiers in clause heads, letting definitions constrain syntax to nominal constants and express dependencies among them.Examples include predicates for nominal constants and for names fresh in a term.Source: §2 · p. 2
- Definitions support both deriving atomic judgments by unfolding and case analysis by unifying judgments with clause heads under a closed-world reading.Both modes consider permutations of nominal constants.Source: §2 · p. 2
- Natural-number induction can prove properties by the length of a bottom-up evaluation of a definition.G is described as intuitionistic and predicative, with higher-order logic, fixed-point definitions, and natural-number induction [4].Source: §2 · pp. 1–2
3 The Structure of Abella
Abella separates executable object-language specifications from reasoning about them in G, and equips theorem proving with tactics that exploit properties of its specification logic. The specification logic represents binding with λ-tree syntax and supports executable structural semantics.
3 The Structure of Abella
- Abella’s architecture combines an executable specification logic whose proof theory is encoded in G with tactics that use knowledge of that logic.The specification logic is embedded in G so object languages can be specified through it rather than directly in G.Source: §3 · p. 2, §3.1 · p. 3
3.1 Specification Logic
- Second-order hereditary Harrop formulas with λ-tree syntax transparently encode structural operational semantics for objects with binding.In the simply typed λ-calculus example, abstraction bodies use specification-logic binding, and hypothetical judgments represent typing assumptions without an explicit context.Source: §3.1 · p. 3, §3 · p. 3
- The specification logic is executable, enabling animation to assess specifications and their use as testing oracles for implementations.Abella encodes its evaluation rules in G and reasons about specifications through that evaluation.Source: §3.1 · p. 3
3.2 Tactics
- Abella’s tactics include generic proof steps and specification-logic tactics that use proved meta-properties such as instantiation and cut admissibility.Five common generic tactics account for more than 90% of usages in the distributed examples suite.Source: §3.2 · p. 4
4 Implementation
Abella’s implementation relies on higher-order unification for case analysis and tactic application, extending pattern unification to address nominal constants and certain non-pattern problems.
4 Implementation
- Higher-order unification underlies case analysis and determines when tactics apply and what results they produce, making its efficiency central to the prover.Abella uses an extended higher-order pattern unification package.Source: §4 · p. 4
- Nominal constants cannot instantiate variables and may be permuted when checking unifiability; examples involve at most two at once.That small number has made naive approaches to permutation sufficient so far.Source: §4 · p. 4
- Case analysis can create non-pattern unification problems, including nominal-constant variants, for which the implementation finds an easy-to-compute most general unifier.The β-contraction clause yields the example B = R M, outside the higher-order pattern fragment.Source: §4 · p. 5
5 Examples
Abella is used to prove properties across the untyped and simply-typed λ-calculus, sequent calculi, and binding-focused challenge problems. The examples also demonstrate normalizability proofs using extended definitions in G.
Results from the λ-calculus
- For untyped λ-terms, Abella proves equivalence of big-step and small-step evaluation, preservation of typing, determinacy, and a disjoint partition into normal and non-normal forms.For simply-typed λ-terms, it also proves uniqueness of typing assignments.Source: §5 · p. 5
Cut admissibility
- Abella proves cut admissibility for a sequent calculus with implication and conjunction, using hypothetical judgments to represent sequent hypotheses.This lets the proof take advantage of Abella’s built-in treatment of meta-properties of the specification logic.Source: §5 · p. 5
The POPLmark challenge
- For the POPLmark challenge, Abella solves parts 1a and 2a, fundamental reasoning tasks involving binding in F<:.The challenge includes reasoning about evaluation, typing, and subtyping for F<:, a λ-calculus with bounded subtype polymorphism.Source: §5 · p. 5
Proving normalizability `a la Tait
- All closed terms in the call-by-value, simply-typed λ-calculus are shown normalizable using a logical-relations argument in the style of Tait.The proof relies on encoding arbitrary cascading substitutions to consider all closed instantiations of an open λ-term; this uses G’s extended definitions.Source: §5 · p. 5
6 Future and Related Work
The paper identifies induction support, user programmability, and automated proof search as areas for extension, then compares Abella with Twelf and Isabelle/HOL’s Nominal package.
Induction and coinduction
- G currently supports induction on natural numbers; structural induction and coinduction are supported by the implementation, while an extended logic describing them is in preparation.Similar logics have been extended with these forms of induction and coinduction.Source: §6 · p. 6
User programmability
- The authors would like to extend Abella with tacticals for composing tactics and a full programming language for custom tactics.These are capabilities found in some tactics-based theorem provers.Source: §6 · p. 6
Proof search
- The authors would like to automate proofs that follow patterns of induction, case analysis, and building from hypotheses; focusing results in similar logics may inform a disciplined approach.Many Abella proofs already follow this pattern.Source: §6 · p. 6
Related work
- Compared with Twelf, Abella’s meta-logic is significantly richer when controlling for dependent types; Isabelle/HOL’s Nominal package leaves substitution-related work to the user.Nominal supports reasoning over α-equivalence classes but does not address the full problem of reasoning with binding.Source: §6 · p. 6