Regular language representations in the constructive type theory of Coq
DOI10.1007/S10817-018-9460-XzbMATH Open1451.68146OpenAlexW2791390006WikidataQ130137861 ScholiaQ130137861MaRDI QIDQ1663246FDOQ1663246
Gert Smolka, Christian Doczkal
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-9460-x
Coqinteractive theorem provingregular languagesWS1Sconstructive type theorytwo-way automataSSReflect
Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) 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?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- Formalizing the Logic-Automaton Connection
- A Formalisation of Finite Automata Using Hereditarily Finite Sets
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Derivatives of Regular Expressions
- Succinctness of the Complement and Intersection of Regular Expressions
- Two-Way Automata in Coq
- A Modular Formalisation of Finite Group Theory
- Deciding Kleene algebras in \texttt{Coq}
- Weak Second‐Order Arithmetic and Finite Automata
- Decision Problems of Finite Automata Design and Related Arithmetics
- Kleene Algebra with Tests and Coq Tools for while Programs
- A note on the reduction of two-way automata to one-way automata
- Proof Pearl: regular expression equivalence and relation algebra
- Automata theory and its applications
- The Complexity of Translating Logic to Finite Automata
- Explicit substitutions
- A coherence theorem for Martin-Löf's type theory
- Structural Analysis of Narratives with the Coq Proof Assistant
- Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
- A Constructive Theory of Regular Languages in Coq
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Endmarkers can make a difference
- Pragmatic Quotient Types in Coq
- Deciding Kleene algebra terms equivalence in Coq
- Automatentheorie und Logik
- A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
Cited In (3)
Uses Software
This page was built for publication: Regular language representations in the constructive type theory of Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663246)
