Proof-directed program transformation: A functional account of efficient regular expression matching. (24th May 2021)

• Record Type: Journal Article
• Authors: FILINSKI, ANDRZEJ
• Is Part Of: Journal of functional programming. Volume 31(2021)
• Publication Date: 2021-05-24
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796820000295
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: 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.