skip to main content
10.1145/1088348.1088355acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
Article

Verifying haskell programs using constructive type theory

Published: 30 September 2005 Publication History

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]
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer-Verlag, 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]
T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2/3):95--120, 1988.]]
[7]
M. de Mol, M. C. J. D. van Eekelen, and M. J. Plasmeijer. Theorem proving for functional programmers. In T. Arts and M. Mohnen, editors, Implementation of Functional Languages, 13th International Workshop, IFL 2001, Stockholm, Sweden, September 24-26, 2001, Lecture Notes in Computer Science, pages 55--71. Springer, 2002.]]
[8]
J.-C. Filliâtre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709--745, July 2003.]]
[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]
W. L. Harrison and R. B. Kieburtz. A logic of demand in Haskell. Journal of Functional Programming, 2005. Under consideration of publication.]]
[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]
C. Kreitz. Formal reasoning about communication systems I: Embedding ML into type theory. Technical report, Cornell University, 1997.]]
[13]
C. Kreitz. Building reliable, high-performance networks with the Nuprl proof development system. Journal of Functional Programming, 14(1):21--68, 2004.]]
[14]
D. Leivant. Finitely stratified polymorphism. Information and Computation, 93(1):93--113, July 1991.]]
[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]
F. Pfenning and C. Schürmann. System description: Twelf --- A meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202--206, Trento, Italy, 1999. Springer-Verlag LNAI 1632.]]
[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 and S. Blott. How to make ad-hoc polymorphism less ad-hoc. In Conference Record of the 16th Annual ACM Symposium on Principles of Programming Languages, pages 60--76. ACM, Jan. 1989.]]

Cited By

View all
  • (2023)Embedding Functional Logic Programming in Haskell via a Compiler PluginPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_3(37-55)Online publication date: 8-Jan-2023
  • (2022)A Monadic Implementation of Functional Logic ProgramsProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551370(1-15)Online publication date: 20-Sep-2022
  • (2022)Reasonable Agda is correct Haskell: writing verified Haskell using agda2hsProceedings of the 15th ACM SIGPLAN International Haskell Symposium10.1145/3546189.3549920(108-122)Online publication date: 6-Sep-2022
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell
September 2005
126 pages
ISBN:159593071X
DOI:10.1145/1088348
  • Program Chair:
  • Daan Leijen
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 September 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. GHC core
  2. haskell
  3. monadic translation
  4. partiality
  5. type theory
  6. verification

Qualifiers

  • Article

Conference

Haskell05
Sponsor:
Haskell05: Haskell Workshop 2005
September 30, 2005
Tallinn, Estonia

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)9
  • Downloads (Last 6 weeks)4
Reflects downloads up to 12 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Embedding Functional Logic Programming in Haskell via a Compiler PluginPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_3(37-55)Online publication date: 8-Jan-2023
  • (2022)A Monadic Implementation of Functional Logic ProgramsProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551370(1-15)Online publication date: 20-Sep-2022
  • (2022)Reasonable Agda is correct Haskell: writing verified Haskell using agda2hsProceedings of the 15th ACM SIGPLAN International Haskell Symposium10.1145/3546189.3549920(108-122)Online publication date: 6-Sep-2022
  • (2022)Regularity and quantification: a new approach to verify distributed protocolsInnovations in Systems and Software Engineering10.1007/s11334-022-00460-819:4(359-377)Online publication date: 29-Sep-2022
  • (2021)Reasoning about the garden of forking pathsProceedings of the ACM on Programming Languages10.1145/34735855:ICFP(1-28)Online publication date: 19-Aug-2021
  • (2021)Haskell⁻¹: automatic function inversion in HaskellProceedings of the 14th ACM SIGPLAN International Symposium on Haskell10.1145/3471874.3472982(41-55)Online publication date: 18-Aug-2021
  • (2021) Ready, Set , Verify! Applying hs-to-coq to real-world Haskell code Journal of Functional Programming10.1017/S095679682000028331Online publication date: 26-Feb-2021
  • (2019)Verifying effectful Haskell programs in CoqProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342592(125-138)Online publication date: 8-Aug-2019
  • (2019)Generic and flexible defaults for verified, law-abiding type-class instancesProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342591(15-29)Online publication date: 8-Aug-2019
  • (2018)Total Haskell is reasonable CoqProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 201810.1145/3176245.3167092(14-27)Online publication date: 2018
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media