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
Meta-theory of
session types as processes
Programming languages
POPLmark Challenge 1a: transitivity of subtyping for system F
sub
The exact challenge, in a first-order specification
POPLmark Challenge 2a: progress and preservation of system F
sub
Evaluation by explicit substitution
PCF: Programming language for Computable Functions
Soudness of Howe's method for open (applicative) bisimilarity
, demonstrating how to quantify over simultaneous substitutions
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