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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

13:00 - 14:30: Gradual Typing and ProvingResearch Papers at Stifel Theatre
Chair(s): Éric TanterUniversity of Chile & Inria Paris
13:00 - 13:22
Talk
A Spectrum of Type Soundness and Performance
Research Papers
Ben GreenmanNortheastern University, USA, Matthias FelleisenNortheastern University, USA
DOI
13:22 - 13:45
Talk
Casts and Costs: Harmonizing Safety and Performance in Gradual Typing
Research Papers
John Peter CamporaULL Lafayette, Sheng ChenUniversity of Louisiana at Lafayette, Eric WalkingshawOregon State University
DOI
13:45 - 14:07
Talk
Graduality from Embedding-Projection Pairs
Research Papers
Max NewNortheastern University, Amal AhmedNortheastern University, USA
DOI
14:07 - 14:30
Talk
Ready, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report)
Research Papers
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