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

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningfagfæ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.
OriginalsprogEngelsk
Artikelnummere12
TidsskriftJournal of Functional Programming
Vol/bind31
Antal sider38
ISSN0956-7968
DOI
StatusUdgivet - 2021

ID: 276274363