Formalization of the pumping lemma for context-free languages
Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, Jos\'e, Carlos Bacelar Almeida
TL;DR
This paper formalizes the Pumping Lemma for context-free languages using the Coq proof assistant, providing a rigorous foundation for its application in language theory and verification.
Contribution
It introduces a formal proof of the Pumping Lemma for CFLs within the Coq proof assistant, enhancing rigor and reliability in formal language theory.
Findings
Formal proof of the Pumping Lemma for CFLs in Coq
Provides a foundation for automated verification of language properties
Strengthens the theoretical basis for language classification
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge