Verifying haskell programs using constructive type theory Export

@inproceedings{abel:vhpuctt, abstract = {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.}, address = {New York, NY, USA}, author = {Abel, Andreas and Benke, Marcin and Bove, Ana and Hughes, John and Norell, Ulf}, booktitle = {Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell}, citeulike-article-id = {342281}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1088348.1088355}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1088348.1088355}, doi = {10.1145/1088348.1088355}, isbn = {1-59593-071-X}, keywords = {agda, dependent-types, functional-programming, haskell, theorem-proving}, location = {Tallinn, Estonia}, pages = {62--73}, posted-at = {2009-05-11 13:24:30}, priority = {0}, publisher = {ACM}, title = {Verifying haskell programs using constructive type theory}, url = {http://dx.doi.org/10.1145/1088348.1088355}, year = {2005} }

TY - CONF ID - abel:vhpuctt L3 - citeulike-article-id:342281 N2 - 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. CY - Tallinn, Estonia SN - 1-59593-071-X AD - New York, NY, USA EP - 73 TI - Verifying haskell programs using constructive type theory PB - ACM T2 - Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell SP - 62 KW - agda KW - dependent-types KW - functional-programming KW - haskell KW - theorem-proving AU - Abel, Andreas AU - Benke, Marcin AU - Bove, Ana AU - Hughes, John AU - Norell, Ulf PY - 2005/// UR - http://dx.doi.org/10.1145/1088348.1088355 ER -