Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Thu 7 Sep 2017 16:00 - 16:30 at L1 - Day 1, Session 5

We demonstrate for the first time that Liquid Haskell, a refinement type checker for Haskell programs, can be used for arbitrary theorem proving by verifying a monoidal string matching algorithm implemented in Haskell. We use refinement types to specify correctness properties, Haskell terms to express proofs of these properties, and Liquid Haskell to check the proofs. We evaluate Liquid Haskell as a theorem prover by replicating our 1428 LoC proof in a dependently-typed language (Coq - 1136 LoC); we compare both proofs, uncovering the relative advantages and disadvantages of the two provers.

Thu 7 Sep

Displayed time zone: Belfast change

15:30 - 16:30
Day 1, Session 5Haskell at L1
Using Coq to Write Fast and Correct Haskell
John Wiegley , Benjamin Delaware Purdue University
A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq
Niki Vazou University of Maryland, Leonidas Lampropoulos University of Pennsylvania, Jeff Polakow