The Design of a Verified Derivative-Based Parsing Tool for Regular Expressions | Zendy

Elton M. Cardoso | Zendy; Maycon Amaro | Zendy; Samuel da Silva Feitosa | Zendy; Leonardo Vieira dos Santos Reis | Zendy; André Du Bois | Zendy; Rodrigo Ribeiro | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

The 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research