Formalization of closure properties for context-free grammars

TL;DR

This paper formalizes core closure properties of context-free grammars within the Coq proof assistant, providing verified algorithms and theorems that enhance the mathematical rigor of context-free language theory.

Contribution

It introduces a formalization of context-free grammars and their closure operations in Coq, including verified algorithms and proofs of correctness.

Findings

Representation of context-free grammars in Coq

Verified algorithms for union, concatenation, and closure

Proofs of correctness for these algorithms

Abstract

Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and the Coq proof assistant. The results obtained so far include the representation of context-free grammars, the description of algorithms for some operations on them (union, concatenation and closure) and the proof of related theorems (e.g. the correctness of these algorithms). A brief survey of related works is presented, as well as plans for further development.