Type logic in Haskell

Type logic is the logic directly associated to types. It turns out that one can go quite far with regards to proving statements with Haskell. I show how to do that, and even how to prove statements in classical logic with Haskell.

Read more