Two-Way Automata in Coq

DOI10.1007/978-3-319-43144-4_10zbMATH Open1478.68122OpenAlexW2478559468MaRDI QIDQ2829256FDOQ2829256

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

Recommendations

• scientific article; zbMATH DE number 1304993
• Two-way automaton computations
• Two-way automata over locally finite semirings
• Partial derivative automata formalized in Coq
• scientific article
• Coalgebraic Automata Theory: Basic Results
• Two-Way Parikh Automata
• scientific article; zbMATH DE number 1863396
• Complementation of coalgebra automata
• Developments in Language Theory

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)

Cites Work

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

Cited In (2)

• 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

This page was built for publication: Two-Way Automata in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829256)