Hybrid Libraries

Examples

• Equality Reasoning on Untyped Lambda Terms

  A declarative and an algorithmic version of equality on lambda terms are defined. In the algorithmic definition, general reflexivity and transitivity rules can be proven to be admissible. Equivalence of these two definitions of equality is also proved. See [FMP15b].

  EqualUntypedR.v: This version uses context relations to relate contexts that appear in different judgments (e.g., the two equality judgments). EqualUntypedG.v: An alternate version version that uses a single generalized context for all judgments appearing in a theorem. EqualUntypedR_ITP10.v and EqualUntypedG_ITP10.v: Old versions described in [FP10].

• Reasoning about Shapes of Lambda Terms

  This example defines the syntax of two versions of the untyped lambda calculus, defines equality and shape predicates relating these two versions, and proves properties about them. (Two lambda terms have the same shape if their syntax trees have the same shape, i.e., they are the same except for variable names at the leaves. A version of this example with a single version of the lambda calculus is described in [FP10].)

  Shapes.v: The definition of syntax and judgments and proofs of internal adequacy of these judgments. (This file is used by both files below and must be compiled.) ShapesR.v: A version with context invariants. ShapesG.v: An alternate version using a single generalized context. Only one of the theorems is proven for illustration and comparison.

• Reasoning about "Smaller" Relation on Lambda Terms

  This example defines a relation describing when a lambda term is a subterm of another lambda term. (The predicate lt defines when a term is strictly smaller than another term, and le defines when a term is strictly smaller or equal to another term. See [FP10].)

  StructUntyped.v

References