Constructively formalizing automata theory

Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan C. Uribe

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present a constructive formalization of the Myhill-Nerode theorem on the minimization of nite automata that follows the account in Hopcroft and Ullman's book Formal Languages and Their Relation to Automata. We chose to formalize this theorem because it illustrates many points critical to formalization of computational mathematics, especially the extraction of an important algorithm from a proof as a method of knowing that the algorithm is correct. It also gave us an opportunity to experiment with a constructive implementation of quotient sets. We carried out the formalization in Nuprl, an interactive theorem prover based on constructive type theory. Nuprl borrows an implementation of the ML language from the LCF system of Milner, Gordon, and Wadsworth, and makes heavy use of the notion of tactic pioneered by Milner in LCF. We are interested in the pedagogical value of electronic formal mathematical texts and have put our formalization on the World Wide Web. Readers are invited to judge whether the formalization adds value in comparison to a careful informal account.
Original languageEnglish
Title of host publication Proof, Language, and Interaction 2000
Subtitle of host publicationEssays in Honour of Robin Milner
Number of pages26
Publication statusPublished - 2000


Dive into the research topics of 'Constructively formalizing automata theory'. Together they form a unique fingerprint.

Cite this