Certified parsing of regular languages

DOI10.1007/978-3-319-03545-1_7MaRDI QIDQ2938042zbMATH OpenOpenAlexFDO

Authors Denis Firsov, Tarmo Uustalu

Publication date 13 January 2015

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-03545-1_7

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• Certified CYK parsing of context-free languages
• Certified context-free parsing: a formalisation of Valiant's algorithm in Agda
• Partial derivative automata formalized in Coq
• Verified, Executable Parsing
• A constructive theory of regular languages in Coq

Cited in

(7)

• Parsing schemata and correctness of parsing algorithms
• Validating LR(1) Parsers
• TRX: a formally verified parser interpreter
• Verified, Executable Parsing
• Certified CYK parsing of context-free languages
• Combining predicate transformer semantics for effects: a case study in parsing regular languages
• Parsing Computer Languages with an Automaton Compiled from a Single Regular Expression

Describes a project that uses

Uses Software

• Agda

This page was built for publication: Certified parsing of regular languages

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