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

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

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• A Modular Formalisation of Finite Group Theory
• Deciding Kleene algebras in \texttt{Coq}
• 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
• 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

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Complementation of Coalgebra Automata 👍 👎
• Coalgebraic Automata Theory: Basic Results 👍 👎
• Two-way automaton computations 👍 👎
• Two-Way Parikh Automata 👍 👎
• Two-way automata over locally finite semirings 👍 👎
• Developments in Language Theory 👍 👎
• Partial Derivative Automata Formalized in Coq 👍 👎

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)