Jana Hofmann: Bachelor's Thesis
Verified Algorithms for ContextFree Grammars in Coq
Advisor: Prof. Dr. Gert Smolka
Abstract:
We give a basic formalization of contextfree grammars and the languages they describe in the proof assistant Coq. We show the decidability of the word and the emptiness problem of contextfree languages by giving and verifying decision procedures. Furthermore, we describe four grammar transformations: The elimination of empty rules, the elimination of unit rules, the separation of characters from the rest of the grammar and the binarization of a grammar. For each transformation, we show that it preserves the language of the grammar. Together, they yield a grammar which is in Chomsky normal form.
We aim for algorithms that are easy to understand and verify. Many of our results are obtained with finite iteration on lists. By using abstractions of fixed point and closure iterations, the correctness of the algorithms is intuitive and formally obtained with short proofs.
References

A formalisation of the theory of contextfree languages in higher order logic (2010)
Aditi Barthwal

Three models for the description of language (1956)
Noam Chomsky

Certified CYK parsing of contextfree languages (2014)
Denis Firsov and Tarmo Uustalu

Certified normalization of contextfree grammars (2015)
Denis Firsov and Tarmo Uustalu

Introduction to Automata Theory, Languages and Computation (1979)
John E. Hopcroft and Jeffrey D. Ullman

Validating LR (1) parsers (2012)
JacquesHenri Jourdan, François Pottier, and Xavier Leroy

Trx: A formally verified parser interpreter (2010)
Adam Koprowski and Henri Binsztok

Automata and Computability (1997)
Dexter C. Kozen

Formalization of contextfree language theory (2016)
Marcus V. M. Ramos

Introduction to computational logic. Lecture Notes [PDF] (2014)
Gert Smolka and Chad E. Brown

The coq reference manual, version 8.5 (July 2016)
The Coq Development Team
Dowloads
Jana Hofmann,
Sat Sep 3 20:07:32 2016