Abstract
In 1968, Earley introduced his parsing algorithm, capable of parsing all context-free grammars in cubic
space and time. This entry contains a formalization of an executable Earley parser. We base our development on Jones'
extensive paper proof of Earley's recognizer and Obua's formalization of context-free grammars
and derivations. We implement and prove correct a functional recognizer modeling Earley's
original imperative implementation and extend it with the necessary data structures to enable the construction
of parse trees, following the work of Scott. We then develop a functional algorithm that
builds a single parse tree, and we prove its correctness. Finally, we generalize this approach to an algorithm
for a complete parse forest and prove soundness.