A Formalisation of the Cocke-Younger-Kasami Algorithm

Maksym Bortin 📧

April 27, 2016


The theory provides a formalisation of the Cocke-Younger-Kasami algorithm (CYK for short), an approach to solving the word problem for context-free languages. CYK decides if a word is in the languages generated by a context-free grammar in Chomsky normal form. The formalized algorithm is executable.


BSD License


Session CYK