<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Marcus Vinícius Midena Ramos</style></author><author><style face="normal" font="default" size="100%">Ruy J. G. B. de Queiroz</style></author><author><style face="normal" font="default" size="100%">Nelma Moreira</style></author><author><style face="normal" font="default" size="100%">José Bacelar Almeida</style></author></authors><secondary-authors><author><style face="normal" font="default" size="100%">Jouko Väänänen</style></author><author><style face="normal" font="default" size="100%">Åsa Hirvonen</style></author><author><style face="normal" font="default" size="100%">Ruy de Queiroz</style></author></secondary-authors></contributors><titles><title><style face="normal" font="default" size="100%">On the Formalization of Some Results of Context-Free Language Theory</style></title><secondary-title><style face="normal" font="default" size="100%">Logic, Language, Information, and Computation – 23rd International Workshop, WoLLIC 2016</style></secondary-title><tertiary-title><style face="normal" font="default" size="100%">Lecture Notes in Computer Science</style></tertiary-title></titles><dates><year><style  face="normal" font="default" size="100%">2016</style></year></dates><urls><web-urls><url><style face="normal" font="default" size="100%">http://www.springer.com/us/book/9783662529201</style></url></web-urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jba/files/16wollic.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Springer-Verlag</style></publisher><volume><style face="normal" font="default" size="100%">9803</style></volume><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimi- nation of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the important result that is the formalization of the Pumping Lemma for context-free languages.&lt;/p&gt;
</style></abstract><notes><style face="normal" font="default" size="100%">&lt;p&gt;n/a&lt;/p&gt;
</style></notes></record></records></xml>