Certified Parsing of Dependent Regular Grammars

Parsers are ubiquitous, but formal reasoning about the behavior of a parser is challenging. One key challenge is parsing dependent formats, which are difficult for traditional techniques to handle because parse values can influence future parsing behavior. We present dependent regular grammars, which extend regular languages with data-dependency by generalizing concatenation to monadic bind. Even this small tweak adds significant expressive power; for example, conditional parsing and dependent repetition are both implementable using monadic bind.However, it is not obvious how to actually parse dependent regular grammars. We implement a Brzozowski derivative based matching algorithm, and we show how many popular parser combinator functions can be implemented in our library while retaining the same simplicity as traditional parser combinators.We implement and formalize these grammars in Coq, as well as a derivative-based matching algorithm. We prove soundness and completeness of the derivative operator in the standard way. We also implement a variety of popular parser combinator functions and give formal specifications to them. Finally, we implement as a case study a verified netstring parser, and prove functional correctness of the parser.