Verifying haskell programs using constructive type theory

Proof assistants based on dependent type theory are closely related to 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 translated into an Agda model of their semantics, by translating via GHC’s Core language into a monadic form specially adapted to represent Haskell’s polymorphism in Agda’s predicative type system. The translation can support reasoning about either total values only, or total and partial values, by instantiating the monad appropriately. We claim that, although these Agda models are generated by a relatively complex translation process, proofs about them are simple and natural, and we offer a number of examples to support this claim.

• Type: Conference
• Year: 2005
• Where: HASKELL
• Authors: Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
• Keywords: Agda Models, HASKELL 2005, Haskell Programs, Proof Assistant