Skip to main content
Version: 2.0.8

Examples

The Abella distribution includes developments that illustrate the proof techniques described in the walkthroughs. Every development below is a .thm file in the examples/ directory of the Abella sources for version 2.0.8.3. 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.

Schematic polymorphism​

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

See also​