DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.31

A Verified Earley Parser

Authors: Martin Rau and Tobias Nipkow

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

An Earley parser is a top-down parsing technique that is capable of parsing arbitrary context-free grammars. We present a functional implementation of an Earley parser verified using the interactive theorem prover Isabelle/HOL. Our formalization builds upon Cliff Jones' extensive, refinement-based paper proof. We implement and prove soundness and completeness of a functional recognizer modeling Jay Earley’s original imperative implementation and extend it with the necessary data structures to enable the construction of parse trees following the work of Elizabeth Scott. Building upon this foundation, we develop a functional parser and prove its soundness. We round off the paper by providing an informal argument and empirical data regarding the running time and space complexity of our implementation.

Cite as

Martin Rau and Tobias Nipkow. A Verified Earley Parser. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{rau_et_al:LIPIcs.ITP.2024.31,
  author =	{Rau, Martin and Nipkow, Tobias},
  title =	{{A Verified Earley Parser}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{31:1--31:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.31},
  URN =		{urn:nbn:de:0030-drops-207596},
  doi =		{10.4230/LIPIcs.ITP.2024.31},
  annote =	{Keywords: Verification, Parsers, Earley, Isabelle}
}

Search Results

Documents authored by Rau, Martin

A Verified Earley Parser

Abstract

Cite as

Thanks for your feedback!

Could not send message