2026-07-22T08:34:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11079 2024-03-06T10:47:19Z ddc:004 open_access

A Verified LL(1) Parser Generator Lasser, Sam Casinghino, Chris Fisher, Kathleen Roux, Cody interactive theorem proving top-down parsing 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sam Lasser and Chris Casinghino and Kathleen Fisher and Cody Roux 2019 Is Part Of LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2019.24 urn:nbn:de:0030-drops-110794 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.24 eng https://creativecommons.org/licenses/by/3.0/legalcode