Validating LR(1) Parsers

DOI10.1007/978-3-642-28869-2_20MaRDI QIDQ2892741zbMATH OpenOpenAlexFDO

Authors Jacques-Henri Jourdan, François Pottier, Xavier Leroy

Publication date 22 June 2012

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28869-2_20

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Formal languages and automata (68Q45)

Recommendations

• Practical optimization of LR(1) parsers
• A Verified LL(1) Parser Generator
• scientific article; zbMATH DE number 4100631
• Developments in Language Theory
• Certified parsing of regular languages
• A functional LR parser
• LR parsing for LCFRS
• LR parsing for conjunctive grammars

Cited in

(11)

• A self-certifying compilation framework for WebAssembly
• On the formalization of some results of context-free language theory
• TRX: a formally verified parser interpreter
• Verified, Executable Parsing
• Certified CYK parsing of context-free languages
• Practical optimization of LR(1) parsers
• A Verified LL(1) Parser Generator
• Bidirectional grammars for machine-code decoding and encoding
• A verified earley parser
• Fast and verified UNSAT certificate checking
• Automatic generation and validation of instruction encoders and decoders

Describes a project that uses

Uses Software

• Coq
• Menhir

This page was built for publication: Validating LR(1) Parsers

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