Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages.
@article{5595,
title = {Formalization of the pumping lemma for context-free languages},
journal = {Journal of Formalized Reasoning},
volume = {9},
year = {2016},
doi = {10.6092/issn.1972-5787/5595},
language = {EN},
url = {http://dml.mathdoc.fr/item/5595}
}
Ramos, Marcus V M; Almeida, José Carlos Bacelar; Moreira, Nelma; de Queiroz, Ruy José Guerra Barretto. Formalization of the pumping lemma for context-free languages. Journal of Formalized Reasoning, Tome 9 (2016) . doi : 10.6092/issn.1972-5787/5595. http://gdmltest.u-ga.fr/item/5595/