Advisors: Christian Doczkal, Gert Smolka
Supervisor: Gert Smolka
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.
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.