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

Filinski, A 2021, 'Proof-directed program transformation: A functional account of efficient regular expression matching', Journal of Functional Programming, vol. 31, e12. https://doi.org/10.1017/S0956796820000295

APA

Filinski, A. (2021). Proof-directed program transformation: A functional account of efficient regular expression matching. Journal of Functional Programming, 31, [e12]. https://doi.org/10.1017/S0956796820000295

Vancouver

Filinski A. Proof-directed program transformation: A functional account of efficient regular expression matching. Journal of Functional Programming. 2021;31. e12. https://doi.org/10.1017/S0956796820000295

Author

Filinski, Andrzej. / Proof-directed program transformation : A functional account of efficient regular expression matching. In: Journal of Functional Programming. 2021 ; Vol. 31.

Bibtex

@article{1f7bad5742b04237802a6a975166211c,
title = "Proof-directed program transformation: A functional account of efficient regular expression matching",
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.",
author = "Andrzej Filinski",
year = "2021",
doi = "10.1017/S0956796820000295",
language = "English",
volume = "31",
journal = "Journal of Functional Programming",
issn = "0956-7968",
publisher = "Cambridge University Press",

}

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