Verified, Executable Parsing

DOI10.1007/978-3-642-00590-9_12MaRDI QIDQ3617698zbMATH OpenOpenAlexFDO

Authors Aditi Barthwal, Michael Norrish

Publication date 31 March 2009

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

Full work available at URL https://doi.org/10.1007/978-3-642-00590-9_12

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Formal languages and automata (68Q45)

Recommendations

• Simple, functional, sound and complete parsing for all context-free grammars
• Validating LR(1) Parsers
• Certified CYK parsing of context-free languages
• TRX: a formally verified parser interpreter
• Certified parsing of regular languages

Cited in

(9)

• From syntactic theories to interpreters: Automating the proof of unique decomposition
• Certified parsing of regular languages
• Simple, functional, sound and complete parsing for all context-free grammars
• TRX: a formally verified parser interpreter
• A mechanisation of some context-free language theory in HOL4
• Certified CYK parsing of context-free languages
• A Verified LL(1) Parser Generator
• Automatic generation and validation of instruction encoders and decoders
• The metafront system: safe and extensible parsing and transformation

This page was built for publication: Verified, Executable Parsing

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