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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:30 - 16:30
Day 1, Session 5Haskell at L1
15:30
30m
Talk
Using Coq to Write Fast and Correct Haskell
Haskell
16:00
30m
Talk
A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq
Haskell
Niki VazouUniversity of Maryland, Leonidas LampropoulosUniversity of Pennsylvania, Jeff Polakow