• Intro: introduction to Equations, demonstrating its features (source).

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).


  • 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).