LIPIcs.ITP.2019.24.pdf
- Filesize: 0.49 MB
- 18 pages
Document
A Verified LL(1) Parser Generator
Authors
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
File
Document Identifiers
Acknowledgements
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)
https://doi.org/10.4230/LIPIcs.ITP.2019.24
https://doi.org/10.4230/LIPIcs.ITP.2019.24
Abstract
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
Keywords
- interactive theorem proving
- top-down parsing
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads