Certified CYK parsing of context-free languages

• Certified implementation of the CYK parsing algorithm for context-free languages.
• Proof-oriented datatypes: substring parsing relation, certified memoization tables.
• Termination from a structurally recursive version of the program.
• The program and the proof are structured with the list monad.
• Modular correctness proof: from the naive version to the memoizing program.

We report a work on certified parsing for context-free grammars. In our development we implement the Cocke–Younger–Kasami parsing algorithm and prove it correct using the Agda dependently typed programming language.