Abella Examples

Process calculi

• The π-calculus
  • Finite π-calculus overview
    • An example of bisimulation checking for the π-calculus
    • Simulation and bisimulation for the π-calculus
    • Simulation in the finite π-calculus is a "pre-congruence"
  • Bisimulation-up-to for the π-calculus with replication
    • Basic definitions
    • Bisimulation up to bisimilarity
  • Relating the π-calculus and the λ-calculus (contributed by Horace Blanc)
    • The linear substitution calculus
    • Definition of the π-calculus
    • Proof that structural equivalence is a bisimulation
    • The translation from λ-calculus to the π-calculus
    • Proof that the translation is a bisimulation
• The Calculus of Communicating Systems (CCS)
  • Bisimulation-up-to
    • Basic definitions
    • Bisimulation up to bisimilarity and some examples
    • CCS contexts are faithful
    • Bisimulation up to context
    • Bisimulation up to bisimilarity and context and some examples
  • A two-level presentation

Programming languages

• POPLmark Challenge 1a: transitivity of subtyping for system F_sub
  • The exact challenge, in a first-order specification
  • A higher-order variant with considerably simpler proofs.
• POPLmark Challenge 2a: progress and preservation of system F_sub
• Evaluation by explicit substitution
• PCF: Programming language for Computable Functions

Logic

• Cut-admissibility for LJ
• Equivalence of natural deduction, Hilbert calculus, and sequent calculus for the implication fragment of minimal logic
• Correctness and completeness of focusing for the implication fragment of minimal logic
• Explicit two-level reasoning
  • Meta-Theory of the restricted HH that allows only dynamically addition of atomic formulas
  • Meta-Theory of the full HH

The λ-calculus

• Normalization for simply-typed terms
  • Strong normalization
  • Weak normalization
• Preservation of strong normalization for a variant of the λσ-calculus
• Church-Rosser
• Standardization
• Evaluation and typing
• Type uniqueness for simply-typed terms
  • With standard techniques
  • With explicit freshness predicate
  • Without using the specification logic
  • Without using nominal abstraction
• Type-preservation for Curry-style System F (Contributed by Ahn Ki Yung)
• Term structure
  • Equivalence on terms based on paths in lambda terms, available in two versions:
    • Second-order version for static terms
    • Higher-order version for terms upto marked β-reduction
  • Partitioning into normal and non-normal form
  • Determinism of translation between HOAS and de Bruijn representations, available in two flavors of specifications.
    • First-order version
    • Higher-order version

First-order reasoning

• Properties of lists
• Addition is associative and commutative
• Totality of the Ackermann function
• Totality of GCD relation
• Every natural number is even or odd

Miscellaneous

• Higher-order logic programming
• Arbitrary cascading (simultaneous) substitutions
• Equivalence of single and double eigenvariable definitions of copy
• Results on possibly infinite natural numbers
• Results on possibly infinite lists
• Correctness of higher-order pattern unification based substitution
• Co-induction in relational semantics
• Use well-founded induction to prove the totality of Euclid's GCD algorithm