Certified derivative based parsing of regular expressions

Published in Programming Languages - 20th Brazilian Symposium on Programming Languages., 2016

We describe the formalization of a certified algorithm for regular expression parsing based on Brzozowski derivatives, in the dependently typed language Idris. The formalized algorithm produces a proof that an input string matches a given regular expression or a proof 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 algorithm, and practical experiments were conducted with this tool.

Download paper here