Formalization of context-free language theory
Formal Languages and Automata Theory
2015-11-02 v1
Abstract
Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of fundamental results related to context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols inaccessible symbols, empty rules and unit rules) and the existence of a Chomsky Normal Form for context-free grammars.
Keywords
Cite
@article{arxiv.1510.09092,
title = {Formalization of context-free language theory},
author = {Marcus V. M. Ramos and Ruy J. G. B. de Queiroz and Nelma Moreira and José Carlos Bacelar Almeida},
journal= {arXiv preprint arXiv:1510.09092},
year = {2015}
}