License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.24
URN: urn:nbn:de:0030-drops-110794
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11079/
Go to the corresponding LIPIcs Volume Portal

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

A Verified LL(1) Parser Generator

pdf-format:
LIPIcs-ITP-2019-24.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{lasser_et_al:LIPIcs:2019:11079,
  author =	{Sam Lasser and Chris Casinghino and Kathleen Fisher and Cody Roux},
  title =	{{A Verified LL(1) Parser Generator}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11079},
  URN =		{urn:nbn:de:0030-drops-110794},
  doi =		{10.4230/LIPIcs.ITP.2019.24},
  annote =	{Keywords: interactive theorem proving, top-down parsing}
}

Keywords: interactive theorem proving, top-down parsing
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: https://github.com/slasser/vermillion

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI