  Context-free languages (CFLs) 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.
