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

15:30 - 16:30: Haskell 2017 - Day 1, Session 5 at L1
haskellsymp-2017-papers150479100000015:30 - 16:00
haskellsymp-2017-papers150479280000016:00 - 16:30
Niki VazouUniversity of Maryland, Leonidas LampropoulosUniversity of Pennsylvania, Jeff Polakow