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.
CITATION STYLE
Lopes, R., Ribeiro, R., & Camarão, C. (2016). Certified derivative-based parsing of regular expressions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9889 LNCS, pp. 95–109). Springer Verlag. https://doi.org/10.1007/978-3-319-45279-1_7
Mendeley helps you to discover research relevant for your work.