Hiromi ISHII

  • 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](http://hackage.haskell.org/package/equational-reasoning), [type-natural](http://hackage.haskell.org/package/type-natural) and [sized-vector](http://hackage.haskell.org/package/sized-vector). These libraries are practically used in my [computational-algebra](https://github.com/konn/computational-algebra) project.