  Proof assistants are software-based tools that are used in the mechanization
of proof construction and validation in mathematics and computer science, and
also in certified program development. Different tools are being increasingly
used in order to accelerate and simplify proof checking. Context-free language
theory is a well-established area of mathematics, relevant to computer science
foundations and technology. This proposal aims at formalizing parts of
context-free language theory in the Coq proof assistant. This report presents
the underlying theory and general characteristics of proof assistants,
including Coq itself, discusses its use in relevant formalization projects,
presents the current status of the implementation, addresses related projects
and the contributions of this work. The results obtained so far include the
formalization of closure properties for context-free grammars (under union,
concatenation and closure) and the formalization of grammar simplification.
Grammar simplification is a subject of high importance in computer language
processing technology as well as in formal language theory, and the
formalization refers to the fact that general context-free grammars generate
languages that can be also generated by simpler and equivalent context-free
grammars. Namely, useless symbol elimination, inaccessible symbol elimination,
unit rules elimination and empty rules elimination operations were described
and proven correct with respect to the preservation of the language generated
by the original grammar.
