TRX: a formally verified parser interpreter

DOI10.1007/978-3-642-11957-6_19MaRDI QIDQ3558235zbMATH OpenOpenAlexFDO

Authors Adam Koprowski, Henri Binsztok

Publication date 4 May 2010

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

Full work available at URL https://doi.org/10.1007/978-3-642-11957-6_19

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Verified, Executable Parsing
• Certified CYK parsing of context-free languages
• Program extraction applied to monadic parsing
• Validating LR(1) Parsers
• Certified parsing of regular languages

Cited in

(9)

• A formally verified interpreter for a shell-like programming language
• On the formalization of some results of context-free language theory
• Simple, functional, sound and complete parsing for all context-free grammars
• Verified, Executable Parsing
• A mechanisation of some context-free language theory in HOL4
• Certified CYK parsing of context-free languages
• Pollack-inconsistency
• A Verified LL(1) Parser Generator
• Fast and verified UNSAT certificate checking

Describes a project that uses

Uses Software

• TRX
• Coq
• CompCert

This page was built for publication: TRX: a formally verified parser interpreter

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