Formalization of the pumping lemma for context-free languages

Authors

  • Marcus V M Ramos Colegiado de Engenharia de Computação, Universidade Federal do Vale do São Francisco (UNIVASF)
  • José Carlos Bacelar Almeida HASLab - INESC TEC, Universidade do Minho
  • Nelma Moreira Departamento de Ciência de Computadores, Faculdade de Ciências, Universidade do Porto
  • Ruy José Guerra Barretto de Queiroz Centro de Informática, Universidade Federal de Pernambuco (UFPE)

DOI:

https://doi.org/10.6092/issn.1972-5787/5595

Keywords:

Coq, context-free languages, pumping lemma

Abstract

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.

Downloads

Published

2016-12-01

How to Cite

Ramos, M. V. M., Almeida, J. C. B., Moreira, N., & de Queiroz, R. J. G. B. (2016). Formalization of the pumping lemma for context-free languages. Journal of Formalized Reasoning, 9(2), 53–68. https://doi.org/10.6092/issn.1972-5787/5595

Issue

Vol. 9 No. 2 (2016)

Section

Articles

License

Copyright (c) 2016 Marcus V M Ramos

Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.

Creative Commons License

This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy