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

Peter Gammie 🌐

August 25, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session BirdKMP

Depends on