一句话：通过证明导向的程序变换，从正则表达式集合语义系统推导出高效的表驱动匹配器，并机器验证每一步等式正确性。
论文针对正则表达式匹配器的高效实现通常依赖专门形式语言与自动机理论的问题，提出一种证明导向的推导方法。作者从正则表达式标准的集合论语义出发，先构造基于续延的回溯匹配器，再经由一系列函数式程序变换得到经典的表驱动状态机。全部推导步骤都配有自包含且机器验证的等式正确性证明，从而在很少使用专门自动机理论的情况下，系统性地获得高效匹配器。该方法展示了程序变换与函数式编程在语言工具实现和正确性保证中的价值。
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.
@article{paperbot1231,
title = {Proof-directed program transformation: A functional account of efficient regular expression matching},
author = {ANDRZEJ FILINSKI},
journal = {Journal of Functional Programming},
volume = {31},
year = {2021},
doi = {10.1017/s0956796820000295}
}