zbMATH — the first resource for mathematics

Certified parsing of regular languages. (English) Zbl 1303.68077
Gonthier, Georges (ed.) et al., Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Berlin: Springer (ISBN 978-3-319-03544-4/pbk). Lecture Notes in Computer Science 8307, 98-113 (2013).
Summary: We report on a certified parser generator for regular languages using the Agda programming language. Specifically, we programmed a transformation of regular expressions into a Boolean-matrix based representation of nondeterministic finite automata (NFAs). And we proved (in Agda) that a string matches a regular expression if and only if the NFA accepts it. The proof of the if-part is effectively a function turning acceptance of a string into a parse tree while the only-if part gives a function turning rejection into a proof of impossibility of a parse tree.
For the entire collection see [Zbl 1298.68028].

68Q45 Formal languages and automata
Full Text: DOI