Gallery of programs and proofs
Dependent PatternMatching

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 wellscoped, welltyped syntax (porting Poulsen et al’s POPL18 paper on IntrisicallyTyped Definitional Interpreters for Imperative Languages) (source).

POPLMark 1a: a solution to POPLMark 1a using wellscoped, welltyped syntax by Rafaël Bocquet, adapted to avoid UIP using equalities in constructors by Matthieu Sozeau. (source).

Views: using dependent patternmatching with views, to handle default cases in patternmatching (source).
Recursion

STLC: strong normalization of simplytyped lambdacalculus with products using hereditary substitutions (source).

String Matching: beginning of example by Nicky Vazou on string matching, uses wellfounded recursion (source).

Rose Trees: nested wellfounded recursion (source).

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

Accumulators: defining and proving programs using accumulators, with wellfounded recursion (source).

Mutual wellfounded recursion: representing mutually recursive wellfounded definitions using dependent patternmatching (source).

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

Higherorder recursion: working with higherorder recursion using structural or wellfounded recursion, here on finitely branching trees as functions from
fin n
. (source). 
Bove Capretta: using the improved BoveCappreta method (not requiring inductionrecursion) to prove termination of McCarthy’s f91. (source).