Proof-directed program transformation: A functional account of efficient regular expression matching
Research output: Contribution to journal › Journal article › Research › peer-review
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.
Original language | English |
---|---|
Article number | e12 |
Journal | Journal of Functional Programming |
Volume | 31 |
Number of pages | 38 |
ISSN | 0956-7968 |
DOIs | |
Publication status | Published - 2021 |
ID: 276274363