Proof-directed program transformation: A functional account of efficient regular expression matching
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Proof-directed program transformation : A functional account of efficient regular expression matching. / Filinski, Andrzej.
In: Journal of Functional Programming, Vol. 31, e12, 2021.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Proof-directed program transformation
T2 - A functional account of efficient regular expression matching
AU - Filinski, Andrzej
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
U2 - 10.1017/S0956796820000295
DO - 10.1017/S0956796820000295
M3 - Journal article
VL - 31
JO - Journal of Functional Programming
JF - Journal of Functional Programming
SN - 0956-7968
M1 - e12
ER -
ID: 276274363