Two-Way Automata in Coq

DOI10.1007/978-3-319-43144-4_10MaRDI QIDQ2829256zbMATH OpenOpenAlexFDO

Authors 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)

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; zbMATH DE number 177806
• Coalgebraic Automata Theory: Basic Results
• Two-Way Parikh Automata
• scientific article; zbMATH DE number 1863396
• Complementation of coalgebra automata
• Developments in Language Theory

Cites work

• scientific article; zbMATH DE number 3254905 (Why is no real title available?)
• scientific article; zbMATH DE number 3254906 (Why is no real title available?)
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• A Modular Formalisation of Finite Group Theory
• A coherence theorem for Martin-Löf's type theory
• A constructive theory of regular languages in Coq
• A formalisation of finite automata using hereditarily finite sets
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• A note on the reduction of two-way automata to one-way automata
• Deciding Kleene algebras in \texttt{Coq}
• Endmarkers can make a difference
• Formalizing the Logic-Automaton Connection
• Nondeterminism and the size of two way finite automata
• Packaging Mathematical Structures
• Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
• Two-way finite automata: old and recent results
• Unified decision procedures for regular expression equivalence
• 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

Describes a project that uses

Uses Software

• MSO_Regex_Equivalence
• Regex_Equivalence
• Finite Automata HF
• Hereditarily Finite Sets
• Presburger Automata
• Myhill-Nerode
• Coq/SSReflect
• 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)