Open AccessThe Design of a Verified Derivative-Based Parsing Tool for Regular Expressions
Author(s) -
Elton M. Cardoso,
Maycon Amaro,
Samuel da Silva Feitosa,
Leonardo Vieira dos Santos Reis,
André Du Bois,
Rodrigo Ribeiro
Publication year - 2021
Publication title -
clei electronic journal
Language(s) - English
Resource type - Journals
ISSN - 0717-5000
DOI - 10.19153/cleiej.24.3.2
Subject(s) - regular expression , parsing , computer science , programming language , expression (computer science) , matching (statistics) , string (physics) , haskell , pattern matching , derivative (finance) , regular language , functional programming , theoretical computer science , artificial intelligence , natural language processing , automaton , mathematics , statistics , financial economics , economics , mathematical physics
We describe the formalization of Brzozowski and Antimirov derivative based algorithms for regular expression parsing, in the dependently typed language Agda. The formalization produces a proof that either an input string matches a given regular expression or that no matching exists. A tool for regular expression based search in the style of the well known GNU grep has been developed with the certified algorithms. Practical experiments conducted with this tool are reported.