A Note on Proofs of Earley's Recognizer

Tobias Nipkow Martin Rau

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}