Abstract We show how to systematically derive an efficient regular expression (regex) matcher using a variety of program transformation techniques, but very little specialized formal language and automata theory. Starting from the standard specification of the set-theoretic semantics of regular expressions, we proceed via a continuation-based backtracking matcher, to a classical, table-driven state machine. All steps of the development are supported by self-contained (and machine-verified) equational correctness proofs.

@article{paperbot1231,
  title = {Proof-directed program transformation: A functional account of efficient regular expression matching},
  author = {ANDRZEJ FILINSKI},
  journal = {Journal of Functional Programming},
  volume = {31},
  year = {2021},
  doi = {10.1017/s0956796820000295}
}