Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs.

Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, Ulf Norell

Browse the full HASKELL paper archive.