Certified CYK parsing of context-free languages

DOI10.1016/j.jlamp.2014.09.002zbMath1371.68137OpenAlexW2055851776MaRDI QIDQ465493

Tarmo Uustalu, Denis Firsov

Publication date: 23 October 2014

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2014.09.002

zbMATH Keywords

parsingAgdacertified programsCocke-Younger-Kasami algorithmdependently typed programming

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theory of programming languages (68N15) Grammars and rewriting systems (68Q42)

Related Items

On the Formalization of Some Results of Context-Free Language Theory

Uses Software

• TRX
• Agda

Cites Work

• Terminating general recursion
• General context-free recognition in less than cubic time
• Validating LR(1) Parsers
• Certified Parsing of Regular Languages
• Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
• TRX: A Formally Verified Parser Interpreter
• Verified, Executable Parsing
• Dependently Typed Programming in Agda
• Total parser combinators
• Recognition and parsing of context-free languages in time n3