Putting the K' into Bird's derivation of Knuth-Morris-Pratt string matching

 Title: Putting the K' into Bird's derivation of Knuth-Morris-Pratt string matching Author: Peter Gammie Submission date: 2020-08-25 Abstract: Richard Bird and collaborators have proposed a derivation of an intricate cyclic program that implements the Morris-Pratt string matching algorithm. Here we provide a proof of total correctness for Bird's derivation and complete it by adding Knuth's optimisation. BibTeX: @article{BirdKMP-AFP, author = {Peter Gammie}, title = {Putting the K' into Bird's derivation of Knuth-Morris-Pratt string matching}, journal = {Archive of Formal Proofs}, month = aug, year = 2020, note = {\url{https://isa-afp.org/entries/BirdKMP.html}, Formal proof development}, ISSN = {2150-914x}, }` License: BSD License Depends on: HOLCF-Prelude