Verifying Monoidal String Matching in Liquid Haskell and Coq See https://nikivazou.github.io/static/Haskell17/a-tale.pdf for a description