Gallery of programs and proofs
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).