Advisors: Christian Doczkal, Gert Smolka
Supervisor: Gert Smolka
Abstract:
We give a constructive formalization of the equivalence between regular expressions,
finite automata and the Myhill-Nerode characterization. We give procedures to convert
between these characterizations and prove their correctness. Our development is done
in the proof assistant Coq. We make use of the SSReflect plugin which provides
support for finite types and other useful infrastructure for our purpose. Our goal was
to make the formalization as concise as possible. The entire development consists of
approximately 2,700 lines of code.
References:
I gave my first Bachelor's seminar talk on March 23, 2012 and my proposal talk on April 27, 2012. I gave my final talk on October 26, 2012
I submitted my thesis (Coq Development) on October 12, 2012.