The Design of a Verified Derivative-Based Parsing Tool for Regular Expressions
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 regul...
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Centro Latinoamericano de Estudios en Informática
2021-12-01
|
| Series: | CLEI Electronic Journal |
| Online Access: | http://www.clei.org/cleiej/index.php/cleiej/article/view/521 |