A Formalisation of the Cocke-Younger-Kasami Algorithm

Maksym Bortin 📧

April 27, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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