Publication details
A Constructive Theory of Regular Languages in Coq
Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka
Certified Programs and Proofs, Third International Conference (CPP 2013), Vol. 8307 of LNCS, pp. 82-97, Springer, December 2013
We present a formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We construct computable functions translating between these representations and show that equivalence of representations is decidable. We also establish the usual closure properties, give a minimization algorithm for DFAs, and prove that minimal DFAs are unique up to state renaming. Our development profits much from Ssreflect's support for finite types and graphs.
Coq Development
Download PDF
Show BibTeX
@INPROCEEDINGS{DoczkalEtAl:2013:A-Constructive,
title = {A Constructive Theory of Regular Languages in Coq},
author = {Christian Doczkal and Jan-Oliver Kaiser and Gert Smolka},
year = {2013},
month = {Dec},
editor = {Geroges Gonthier and Michael Norrish},
publisher = {Springer},
booktitle = {Certified Programs and Proofs, Third International Conference (CPP 2013)},
series = {LNCS},
volume = {8307},
pages = {82-97},
}
Login to edit
Legal notice, Privacy policy
