Abstract
We describe our 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.
[pdf, code (Agda 2.4.2; standard library 0.8.1)]