QED Prover

Experiments writing a proof system, particularly designed to prove properties about Haskell code, such as the HLint rewrite rules.

Tom Ellis described the approach as "coinduction on the execution".