Verifying haskell programs using constructive type theory

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.

REFERENCES

• 1: G. Barthe, J. Hatcliff, and P. Thiemann. Monadic type systems: Pure type systems for impure settings. In A. Gordon, A. Pitts, and C. Talcott, editors, HOOTS II, Second Workshop on Higher-Order Operational Techniques in Semantics, volume 10 of Electronic Notes in Theoretical Computer Science, pages 54--120, 1997.
• 2: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 3: V. Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 2005. To appear.
• 4: K. Claessen and J. Hughes. Quickcheck: A lightweight tool for random testing of haskell programs, 2000.
• 5: C. Coquand and T. Coquand. Structured type theory. In Proc. Workshop on Logical Frameworks and Meta-languages, 1999.
• 6: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 7: Maarten de Mol , Marko C. J. D. van Eekelen , Marinus J. Plasmeijer, Theorem Proving for Functional Programmers, Selected Papers from the 13th International Workshop on Implementation of Functional Languages, p.55-71, September 24-26, 2001
• 8: Jean-Christophe Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of Functional Programming, v.13 n.4, p.709-745, July 2003 [doi>10.1017/S095679680200446X]
• 9: T. Hallgren, J. Hook, M. P. Jones, and R. B. Kieburtz. An overview of the programatica toolset. Presented at the High Confidence Software and Systems Conference, HCSS04, 2004.
• 10: William L. Harrison , Richard B. Kieburtz, The logic of demand in Haskell, Journal of Functional Programming, v.15 n.6, p.837-891, November 2005 [doi>10.1017/S0956796805005666]
• 11: W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, London, 1980.
• 12: Christoph Kreitz, Formal Reasoning about Communication Systems I: Embedding ML into Type Theory., Cornell University, Ithaca, NY, 1997
• 13: Christoph Kreitz, Building reliable, high-performance networks with the Nuprl proof development system, Journal of Functional Programming, v.14 n.1, p.21-68, January 2004 [doi>10.1017/S0956796803004854]
• 14: Daniel Leivant, Finitely stratified polymorphism, Information and Computation, v.93 n.1, p.93-113, July 1991 [doi>10.1016/0890-5401(91)90053-5]
• 15: J. Longley and R. Pollack. Reasoning about cbv functional programs in isabelle/hol. In K. Slind, A. Bunker, and G. Gopalakrishnan, editors, Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, volume 3223 of Lecture Notes in Computer Science, pages 201--216. Springer, 2004.
• 16: P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
• 17: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 18: T. Uustalu. Monad translating inductive and coinductive types. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, volume 2646 of Lecture Notes in Computer Science, pages 299--315. Springer, 2003.
• 19: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Theory, Verification

Keywords:
GHC core, haskell, monadic translation, partiality, type theory, verification