HackerPapers

arXiv:1711.09286cs.PL

Total Haskell is Reasonable Coq

Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies -- a lawful Monad instance, "Hutton's razor", and an existing data structure library -- and prove their correctness. These examples show that this approach is viable: both that hs-to-coq applies to existing Haskell code, and that the output it produces is amenable to verification.

arXiv comments
13 pages plus references. Published at CPP'18, In Proceedings of 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'18). ACM, New York, NY, USA, 2018
Journal reference
DOI
doi:10.1145/3167092
Subjects
cs.PLProgramming Languages

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Nov 2019 to Nov 2019. Found in 1 HN submission from Nov 2017 to Nov 2017. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Haskell and Rust 1 comment

    • > Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you saying you are unaware of any such studies? On the contrary! Consider for instance: "Total Haskell is Reasonable Coq"[1] 1.…

      pittmaView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.