cicyt UNIZAR
Full-text links:

Download:

Current browse context:

cs.PL

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Programming Languages

Title: Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code

Abstract: Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell's containers library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library's test suite, and interfaces from Coq's standard library. Our work shows that it is feasible to verify mature, widely-used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend hs-to-coq to handle partiality, and -- since we found no bugs -- attest to the superb quality of well-tested functional code.
Comments: 30 pages, submitted to ICFP'18
Subjects: Programming Languages (cs.PL)
Cite as: arXiv:1803.06960 [cs.PL]
  (or arXiv:1803.06960v1 [cs.PL] for this version)

Submission history

From: Joachim Breitner [view email]
[v1] Mon, 19 Mar 2018 14:42:25 GMT (100kb,D)