文章基本信息

标题：A Verified LL(1) Parser Generator
本地全文：下载
作者：Sam Lasser ; Chris Casinghino ; Kathleen Fisher 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：141
页码：1-18
DOI：10.4230/LIPIcs.ITP.2019.24
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：interactive theorem proving; top-down parsing