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.