This is the unofficial version of the talk accompanying the paper "Verified and Efficient Matching of Regular Expressions with Lookaround" by Agnishom Chattopadhyay, Angela W. Li and Konstantinos Mamouras, to be presented at CPP 2025.
==Abstract==
Regular expressions can be extended with lookarounds for contextual matching. This paper discusses a Coq formalization of the theory of regular expressions with lookarounds. We provide an efficient and purely functional algorithm for matching expressions with lookarounds and verify its correctness. The algorithm runs in time linear in both the size of the regular expression as well as the input string. Our experimental results provide empirical support to our complexity analysis. To the best of our knowledge, this is the first formalization of a linear-time matching algorithm for regular expressions with lookarounds.
================
Formalization: github.com/Agnishom/lregex
Paper: doi.org/10.1145/3703595.3705884
Some Other Relevant Works
1. Efficient Matching of Regular Expressions with Lookaround Assertions [Mamouras and Chattopadhyay, POPL'24]
2. Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping [Fujinami and Hasuo, ETAPS'24]
3. Linear Matching of JavaScript Regular Expressions [Barrière and Pit-Claudel, PLDI'24]
4. Lean Formalization of Extended Regular Expression Matching with Lookarounds [Zhuchko et al, CPP'24]
Some Other Relevant Digital Artifacts
1. github.com/epfl-systemf/RegElk
2. zenodo.org/records/10458317
3. github.com/ezhuchko/extended-regexes/tree/main