Email Gateway (Aug 08 2023 at 14:38): Email Gateway (Aug 08 2023 at 14:38):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new entry: Earley Parser, by Martin Rau. It weighs in at more than 6500 lines.
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.
You will find it on-line here: https://www.isa-afp.org/entries/Earley_Parser.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC