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.
parsing certified programs cockeyoungerkasami algorithm dependently typed programming agda