Advanced functional proofs
A project-driven advanced course in verified functional programming. Implement polymorphic map, filter-map fusion and a left fold; prove append and composition laws; represent element-wise evidence with an indexed proposition; preserve length in a dependent vector type; and finish by verifying map fusion and structural invariants for a binary tree.
Sign in to track your progress
- Higher-order lists3 lessons
- Build map and prove its append lawImplement a polymorphic map, then prove the compositional law callers need.20 min
- Fuse two mapsRemove an intermediate traversal with a general function-composition proof.16 min
- Fuse filtering and mappingWrite a branching list combinator and prove its append law in both predicate cases.22 min
- Folds and invariants2 lessons
- A fold with a generalized accumulatorBuild a left fold and strengthen the induction hypothesis enough to prove chunking.22 min
- Carry a proof for every elementDefine an indexed All predicate and map evidence through a transformation.24 min
- Dependent data1 lesson
- Make lengths part of the typeImplement vector map so preserving length is enforced before any theorem runs.24 min
- Verified project1 lesson
- Finale: verify a polymorphic tree mapProve map fusion and size preservation with two induction hypotheses per node.28 min