A verified earley parser

DOI10.4230/LIPICS.ITP.2024.31MaRDI QIDQ6859996zbMATH OpenFDO

Authors Martin Rau, Tobias Nipkow

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2024.31

zbMATH Keywords

earleyIsabelleparsersverification

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A general context-free parsing algorithm running in linear time on every LR(k) grammar without using lookahead
• A Verified LL(1) Parser Generator
• An efficient context-free parsing algorithm
• Certified CYK parsing of context-free languages
• Concrete semantics. With Isabelle/HOL
• Efficient parsing algorithms for general context-free parsers
• scientific article; zbMATH DE number 1693497 (Why is no real title available?)
• scientific article; zbMATH DE number 5277949 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Packrat parsing: simple, powerful, lazy, linear time
• Parsing expression grammars: a recognition-based syntactic foundation
• Practical Earley Parsing
• Simple, functional, sound and complete parsing for all context-free grammars
• Total parser combinators
• Validating LR(1) Parsers

This page was built for publication: A verified earley parser

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6859996)