Learning Equations

  • You can discover and learn Equations through interactive tutorials directly in your browser, or locally with Equations installed.

You can also check out the following older introduction material to Equations

Dependent Pattern-Matching

  • Polynomials: a reflexive tactic for solving boolean tautologies (initial version by Rafaël Bocquet) (source).

  • HoTT_light: basics of the HoTT library implemented using a logic in Type (source).

  • MoreDep: part of chapter 8 of Adam Chlipala’s CPDT (original version by Cyprien Mangin) (source).

  • Definitional interpreter: definitional interpreter for an impure language using well-scoped, well-typed syntax (porting Poulsen et al’s POPL18 paper on Intrisically-Typed Definitional Interpreters for Imperative Languages) (source).

  • POPLMark 1a: a solution to POPLMark 1a using well-scoped, well-typed syntax by Rafaël Bocquet, adapted to avoid UIP using equalities in constructors by Matthieu Sozeau. (source).

  • Views: using dependent pattern-matching with views, to handle default cases in pattern-matching (source).

Recursion

  • STLC: strong normalization of simply-typed lambda-calculus with products using hereditary substitutions (source).

  • String Matching: beginning of example by Nicky Vazou on string matching, uses well-founded recursion (source).

  • Rose Trees: nested well-founded recursion (source).

  • Nested mutual recursion: structural mutual and nested recursion (source).

  • Accumulators: defining and proving programs using accumulators, with well-founded recursion (source).

  • Mutual well-founded recursion: representing mutually recursive well-founded definitions using dependent pattern-matching (source).

  • General recursion: working with general recursive functions, without worrying about termination proofs (source).

  • Higher-order recursion: working with higher-order recursion using structural or well-founded recursion, here on finitely branching trees as functions from fin n. (source).

  • Bove Capretta: using the improved Bove-Cappreta method (not requiring induction-recursion) to prove termination of McCarthy’s f91. (source).