Verifying Haskell programs using constructive type theory

Abstract Proof assistants based on dependent type theory are closely relatedto functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In this paper,we show how Agda, such a proof assistant, can be used to prove theorems about Haskell programs. Haskell programs are translatedinto an Agda model of their semantics, by translating via GHC's Core language into a monadic form specially adapted to representHaskell's polymorphism in Agda's predicative type system. The translation can support reasoning about either total values only, ortotal and partial values, by instantiating the monad appropriately. We claim that, although these Agda models are generated by a rel-atively complex translation process, proofs about them are simple and natural, and we offer a number of examples to support thisclaim