Contents

• Contents
• Introduction
  • Background
  • Value of the Formalization
  • Interpretations of the Mathematics
  • Outline
• Type Theory Preliminaries
  • Basic Types
  • Cartesian Products
  • Function Types
  • Propositions and Universes
  • Subtypes and Finiteness
  • Algebraic Structures and Dependent Types
  • Reading Nuprl Proofs
• Languages and their Representation
  • Alphabets and Languages
  • Procedures and Algorithms
  • Representations of Languages
• Finite Automata
  • Definition
  • Semantics of Automata
  • Equivalence Relations and Quotient Types
  • Finite Index Equivalence Relations
  • Equivalence Relations on Strings Induced by Finite Automata
• The Myhill-Nerode Theorem
  • Hopcroft and Ullman Version
  • Formalizing
  • Formalizing
  • Formalizing
• State Minimization
  • Textbook Proof
  • Filling in Gaps in Textbook Proof
  • Minimization Theorem
  • Computational Behavior
• Future Work and Conclusion
• References
• About this document ...