Ramos MVM, de Queiroz RJGB, Moreira N, Almeida JB.
2016.
On the Formalization of Some Results of Context-Free Language Theory. Logic, Language, Information, and Computation – 23rd International Workshop, WoLLIC 2016. 9803
AbstractThis 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.
Ramos MVM, Almeida JB, Moreira N, de Queiroz RJGB.
2016.
Formalization of the Pumping Lemma for Context-Free Languages. Journal of Formalized Reasoning. 9(2):53-68.
AbstractContext-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.