Certified CYK parsing of context-free languagesFirsov, Denis; Uustalu, TarmoJournal of logical and algebraic methods in programming2014 / p. 459-468