Verified Parallel String Matching in Haskell
Programming Languages
2016-10-25 v1
Abstract
In this paper, we prove correctness of parallelizing a string matcher using Haskell as a theorem prover. We use refinement types to specify correctness properties, Haskell terms to express proofs and Liquid Haskell to check correctness of proofs. First, we specify and prove that a class of monoid morphisms can be parallelized via parallel monoid concatenation. Then, we encode string matching as a morphism to get a provably correct parallel transformation. Our 1839LoC prototype proof shows that Liquid Haskell can be used as a fully expressive theorem prover on realistic Haskell implementations.
Keywords
Cite
@article{arxiv.1610.07118,
title = {Verified Parallel String Matching in Haskell},
author = {Niki Vazou and Jeff Polakow},
journal= {arXiv preprint arXiv:1610.07118},
year = {2016}
}