# A formalisation of the Cocke-Younger-Kasami algorithm

 Title: A formalisation of the Cocke-Younger-Kasami algorithm Author: Maksym Bortin Submission date: 2016-04-27 Abstract: 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. BibTeX: @article{CYK-AFP, author = {Maksym Bortin}, title = {A formalisation of the Cocke-Younger-Kasami algorithm}, journal = {Archive of Formal Proofs}, month = apr, year = 2016, note = {\url{https://isa-afp.org/entries/CYK.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.