Publication details

Saarland University Computer Science

Regular Language Representations in the Constructive Type Theory of Coq

Christian Doczkal, Gert Smolka

Journal of Automated Reasoning 61(1):521-553, June 2018

We explore the theory of regular language representations in the constructive type theory of Coq. We cover various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. We give translations between all representations, show decidability results, and provide operations for various closure properties. Our results include a constructive decidability proof for the logic WS1S, a constructive refinement of the Myhill-Nerode characterization of regularity, and translations from two-way automata to one-way automata with verified upper bounds for the increase in size. All results are verified with an accompanying Coq development of about 3000 lines.

Coq Development (on GitHub)

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy