@conference {RQMA16,
	title = {On the Formalization of Some Results of Context-Free Language Theory},
	booktitle = {Logic, Language, Information, and Computation {\textendash} 23rd International Workshop, WoLLIC 2016},
	series = {Lecture Notes in Computer Science},
	volume = {9803},
	year = {2016},
	note = {<p>n/a</p>
},
	publisher = {Springer-Verlag},
	organization = {Springer-Verlag},
	abstract = {<p>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.</p>
},
	url = {http://www.springer.com/us/book/9783662529201},
	attachments = {https://haslab.uminho.pt/sites/default/files/jba/files/16wollic.pdf},
	author = {Marcus Vin{\'\i}cius Midena Ramos and Ruy J. G. B. de Queiroz and Nelma Moreira and Jos{\'e} Bacelar Almeida},
	editor = {Jouko V{\"a}{\"a}n{\"a}nen and {\r A}sa Hirvonen and Ruy de Queiroz}
}