Two-Way Automata in Coq

DOI10.1007/978-3-319-43144-4_10zbMath1478.68122OpenAlexW2478559468MaRDI QIDQ2829256

Christian Doczkal, Gert Smolka

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_10

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Completeness and decidability results for CTL in constructive type theory, Regular language representations in the constructive type theory of Coq

Uses Software

• Coq
• Coq/SSReflect
• Myhill-Nerode
• Presburger Automata
• Hereditarily Finite Sets
• Finite Automata HF
• Regex_Equivalence
• MSO_Regex_Equivalence

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
• Endmarkers can make a difference
• A note on the reduction of two-way automata to one-way automata
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Unified Decision Procedures for Regular Expression Equivalence
• Deciding Kleene Algebras in Coq
• A Constructive Theory of Regular Languages in Coq
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Formalizing the Logic-Automaton Connection
• Packaging Mathematical Structures
• A Formalisation of Finite Automata Using Hereditarily Finite Sets
• A Modular Formalisation of Finite Group Theory
• A coherence theorem for Martin-Löf's type theory
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Nondeterminism and the size of two way finite automata