A Note on Proofs of Earley's Recognizer
This paper presents the formalization and verification (in the proof
assistant Isabelle) of an abstract inductive version of Earley's recognizer,
relates it to the standard definition and derives an efficient one-pass algorithm
for $\varepsilon$-free grammars. In particular it compares
Jones development of Earley's recognizer to our own and to the literature.
Springer
Author pdf
BibTeX:
@incollection{NipkowR-CBJ24,
author={Tobias Nipkow and Martin Rau},
title={A Note on Proofs of {Earley's} Recognizer},
booktitle={The Practice of Formal Methods. Essays in Honour of Cliff Jones, Part II},
editor={Ana Cavalcanti and James Baxter},
publisher=Springer,series=LNCS,volume={14781},pages={45--55},year=2024}