Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Wed 26 Sep 2018 14:07 - 14:30 at Stifel Theatre - Gradual Typing and Proving Chair(s): Éric Tanter

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.

Wed 26 Sep

icfp-2018-papers
13:00 - 14:30: Research Papers - Gradual Typing and Proving at Stifel Theatre
Chair(s): Éric TanterUniversity of Chile & Inria Paris
icfp-2018-papers13:00 - 13:22
Talk
Ben GreenmanNortheastern University, USA, Matthias FelleisenNortheastern University, USA
DOI
icfp-2018-papers13:22 - 13:45
Talk
John Peter CamporaULL Lafayette, Sheng ChenUniversity of Louisiana at Lafayette, Eric WalkingshawOregon State University
DOI
icfp-2018-papers13:45 - 14:07
Talk
Max S. NewNortheastern University, Amal AhmedNortheastern University, USA
DOI
icfp-2018-papers14:07 - 14:30
Talk
Joachim BreitnerDFINITY Foundation, Antal Spector-Zabusky, Yao LiUniversity of Pennsylvania, Christine RizkallahUniversity of New South Wales, John WiegleyBAE Systems, Stephanie WeirichUniversity of Pennsylvania, USA
DOI