Jan-Oliver Kaiser: Bachelor's Thesis

Programming Systems

Jan-Oliver Kaiser

Bachelor's Thesis

Constructive Formalization of Regular Languages

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:

• Constructively formalizing automata theory (1997)
  Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan C. Uribe
• A Decision Procedure for Regular Expression Equivalence in Type Theory (2011)
  Thierry Coquand, Vincent Siles
• A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions (Proof Pearl) (2011)
  Chunhan Wu, Xingyuan Zhang, Christian Urban
• Proof Pearl: Regular Expression Equivalence and Relation Algebra (2011)
  Alexander Krauss, Tobias Nipkow
• Deciding Kleene Algebras in Coq (2011)
  Thomas Braibant, Damien Pous
• Deciding Regular Expressions (In-)Equivalence in Coq (2011)
  Nelma Moreira, David Pereira, Simãelo de Sousa

Presentations

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

Thesis

I submitted my thesis (Coq Development) on October 12, 2012.