Skip to main content
Version: 2.1.0-dev

Examples

The Abella distribution includes developments that illustrate the proof techniques described in the walkthroughs. Every development below is a .thm or .thmod file in the examples/ directory of the Abella sources for version 2.1.0-dev. The links open the generated trace pages for this version, and each development page links to its specification's .lp.html page where applicable. The generated pages are produced by abella_doc and should not be edited by hand.

To run an example, work in its directory and start Abella with the matching specification:

$ cd examples/lambda-calculus
$ abella eval.thm

Many examples depend on a specification (.sig and .mod) or on a compiled development loaded with Import. Running the example from its own directory resolves those dependencies. The generated documentation for each development can be produced with abella_doc.

First-order logic​

  • ackermann: totality of the Ackermann function, with nested induction.
  • add: properties of addition, with the natural numbers encoded as a predicate.
  • even-odd: every natural number is even or odd, with nested induction.
  • gcd: totality of Euclid's GCD algorithm, using an ordering on numbers.
  • lists: results about append, reverse, and permutation.

Higher-order abstract syntax​

  • bred_alt: an alternative formulation of beta reduction.
  • breduce: beta reduction for lambda terms in higher-order syntax.
  • debruijn_ho: determinism of a translation from lambda terms to de Bruijn terms.

Lambda calculus​

Core results​

  • cr: Takahashi's proof of the Church-Rosser theorem using complete developments.
  • eval: determinacy of evaluation and typing, subject reduction, and related results.
  • sred: Ralph Loader's proof of standardization.
  • fcurry: type preservation for Curry-style System F.

Normalization​

  • stlc-strong-norm: Girard's proof of strong normalization for the simply-typed lambda calculus.
  • stlc-weak-norm: Tait's logical relations argument for weak normalization.

Term structure​

  • debruijn: translation between higher-order and de Bruijn lambda terms.
  • normal: partitioning lambda terms into normal and non-normal forms.
  • path: paths through lambda terms and their preservation.

Type uniqueness​

Logic​

  • cut: cut admissibility for the sequent calculus.
  • equiv: equivalence of natural deduction, Hilbert calculus, and sequent calculus.
  • focus: soundness and completeness for a focused logic.
  • hh_meta: metatheory of higher-order Horn clauses, including reasoning about multisets.
  • seq: reasoning about an explicit specification logic.

Miscellaneous​

  • cascade: cascading substitutions on untyped lambda terms, with nabla in a definition head.
  • colist: results about potentially infinite lists.
  • conat: co-natural numbers, that is, natural numbers extended with infinity.
  • copy: equivalence of single and double eigenvariable definitions of copying.
  • flex-rigid: case analysis on flexible-rigid equalities outside LLambda.
  • subst: correctness of the LLambda substitution predicate.
  • umt: co-induction in relational semantics.
  • well-founded: totality of the GCD algorithm by well-founded induction.

Process calculi​

CCS​

Two-level CCS​

  • ccs: CCS results stated in the two-level logic.

Pi calculus​

Two-level pi calculus​

  • finite-pic: simulation and bisimulation for the finite pi calculus.
  • finite-pic-cong: simulation is a pre-congruence.
  • pic: bisimulation checking for the pi calculus.

Pi calculus with lambda​

  • picalc: channels and processes for the pi calculus with lambda terms.
  • trans: a translation defined by recursion on terms.
  • trans_is_bisimulation: the translation preserves bisimulation.
  • picalc_str_eq_is_bisimulation: structural equivalence implies bisimulation.
  • lsc: definitions of terms for the lambda calculus fragment.

Session types​

  • sess: type preservation for session-typed proof terms for classical propositional MALL.

Programming languages​

  • ees: evaluation by explicit substitution for a small language.
  • pcf: properties of PCF.
  • poplmark-1a: reflexivity and transitivity for Fsub.
  • poplmark-2a: progress and preservation for Fsub.

Howe's method​

  • howe: Howe's method for a PCF-like language.
  • sim: simulation for the same language.
  • subst: substitution lemmas for the same language.

Reasoning-level modules​

The examples/modules/README.md file documents the module examples and their expected error cases.

  • List.thmod: a parameterized list theory with an internal kind and an axiom.
  • ListUse.thm: imports List at two element types.
  • Box.thmod: a parameterized module with an internal kind.
  • BoxUse.thmod: two instances with distinct internal types.
  • Nested.thmod: a parameterized module with a nested parameterized module.
  • NestedUse.thmod: imports a module and uses its nested items.
  • Eq.thmod: an abstract equality predicate with an axiom.
  • EqUse.thmod: maps the predicate and axiom to a defined predicate and theorem.
  • EqUseDecl.thmod: maps them to a declared predicate and an axiom.
  • PropKey.thmod: zero-argument predicate and axiom keys.
  • PropKeyUse.thmod: maps zero-argument keys.
  • Keys.thmod: a template with two declared predicates and an axiom.
  • KeysUse.thmod: unmapped keys and an aliased re-import.
  • ShowModule.thm: inline and imported module summaries.

Computation​

  • nats: computation on natural numbers, with suspension guards.
  • rels: asynchronous computation on relations.
  • mll: computation for a permutation relation.

Schematic polymorphism​

  • schm_poly_tst: tests for schematic polymorphism in definitions and theorems.

See also​