Gallery of programs

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

Polynomials: a reflexive tactic for solving boolean tautologies (source).

HoTT_light: basics of the HoTT library implemented using a logic in
Type
(source). 
STLC: strong normalization of simplytyped lambdacalculus with products using hereditary substitutions (source).

MoreDep: part of chapter 8 of Adam Chlipala’s CPDT (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).

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