Proof-directed program transformation: A functional account of efficient regular expression matching
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
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.
Originalsprog | Engelsk |
---|---|
Artikelnummer | e12 |
Tidsskrift | Journal of Functional Programming |
Vol/bind | 31 |
Antal sider | 38 |
ISSN | 0956-7968 |
DOI | |
Status | Udgivet - 2021 |
ID: 276274363