Lean Formalization of Extended Regular Expression Matching with Lookarounds

Ekaterina Zhuchko

Tallinn University of Technology



Abstract: We present a formalization of a matching algorithm for extended regular expression matching based on locations and symbolic derivatives which supports intersection, complement and lookarounds and whose implementation mirrors an extension of the recent .NET NonBacktracking regular expression engine. The formalization of the algorithm and its semantics uses the Lean 4 proof assistant.