Verified Parallel String Matching in Haskell

TL;DR

This paper demonstrates how Liquid Haskell can be used as a theorem prover to verify the correctness of parallel string matching algorithms implemented in Haskell, ensuring reliable parallelization.

Contribution

It introduces a method to specify and prove correctness of parallel string matching in Haskell using refinement types and Liquid Haskell, bridging theorem proving and practical implementation.

Findings

Liquid Haskell can verify correctness of parallel string matching

Parallel monoid concatenation is proven correct for a class of morphisms

Prototype implementation with 1839 lines of code confirms feasibility

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.