Proof-directed program transformation: A functional account of efficient regular expression matching

Research output: Contribution to journalJournal articleResearchpeer-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 languageEnglish
Article numbere12
JournalJournal of Functional Programming
Volume31
Number of pages38
ISSN0956-7968
DOIs
Publication statusPublished - 2021

ID: 276274363