Prove Your Haskell for Great Safety!

This series of tutorial discusses how to write dependently-typed programs and prove their correctness with Haskell. In addition, this series introduces the way to make the proof human-readable and eliminate the run-time overhead introduced by the proof.

The content of this series is implemented in packages equational-reasoning, type-natural and sized-vector. These libraries are practically used in my computational-algebra project.