Document Open Access Logo

A Verified LL(1) Parser Generator

Authors Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux

Thumbnail PDF


  • Filesize: 0.49 MB
  • 18 pages

Document Identifiers

Author Details

Sam Lasser
  • Tufts University, Medford, MA, USA
Chris Casinghino
  • Draper, Cambridge, MA, USA
Kathleen Fisher
  • Tufts University, Medford, MA, USA
Cody Roux
  • Draper, Cambridge, MA, USA


We thank our anonymous reviewers for their helpful feedback.

Cite AsGet BibTex

Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux. A Verified LL(1) Parser Generator. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 24:1-24:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


An LL(1) parser is a recursive descent algorithm that uses a single token of lookahead to build a grammatical derivation for an input sequence. We present an LL(1) parser generator that, when applied to grammar G, produces an LL(1) parser for G if such a parser exists. We use the Coq Proof Assistant to verify that the generator and the parsers that it produces are sound and complete, and that they terminate on all inputs without using fuel parameters. As a case study, we extract the tool’s source code and use it to generate a JSON parser. The generated parser runs in linear time; it is two to four times slower than an unverified parser for the same grammar.

Subject Classification

ACM Subject Classification
  • Theory of computation → Grammars and context-free languages
  • Software and its engineering → Parsers
  • Software and its engineering → Formal software verification
  • interactive theorem proving
  • top-down parsing


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail