Formal derivation of a pattern matching algorithm
The functional version of the Knuth-Morris-Pratt pattern matching algorithm is formally derived using the Bird's calculus of lists. The derivation process is thoroughly explained, various solving strategies are discussed, the paper is self-contained.
scientific article; zbMATH DE number 4113937