Sciweavers

Share
HASKELL
2005
ACM

Verifying haskell programs using constructive type theory

10 years 3 months ago
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.
Andreas Abel, Marcin Benke, Ana Bove, John Hughes,
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where HASKELL
Authors Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell
Comments (0)
books