Regular language representations in the constructive type theory of Coq

DOI10.1007/s10817-018-9460-xzbMath1451.68146OpenAlexW2791390006MaRDI QIDQ1663246

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

zbMATH Keywords

constructive type theoryregular languagesinteractive theorem provingCoqWS1Stwo-way automataSSReflect

Mathematics Subject Classification ID

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)

Related Items (1)

Deep Generation of Coq Lemma Names Using Elaborated Terms

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Endmarkers can make a difference
• A note on the reduction of two-way automata to one-way automata
• Deciding Kleene algebra terms equivalence in Coq
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• Proof Pearl: regular expression equivalence and relation algebra
• Two-Way Automata in Coq
• Deciding Kleene Algebras in Coq
• A Constructive Theory of Regular Languages in Coq
• Succinctness of the Complement and Intersection of Regular Expressions
• Automatentheorie und Logik
• Structural Analysis of Narratives with the Coq Proof Assistant
• A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Formalizing the Logic-Automaton Connection
• Weak Second‐Order Arithmetic and Finite Automata
• A Formalisation of Finite Automata Using Hereditarily Finite Sets
• A Modular Formalisation of Finite Group Theory
• Decision Problems of Finite Automata Design and Related Arithmetics
• A coherence theorem for Martin-Löf's type theory
• The Complexity of Translating Logic to Finite Automata
• Explicit substitutions
• Kleene Algebra with Tests and Coq Tools for while Programs
• Pragmatic Quotient Types in Coq
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Derivatives of Regular Expressions
• Automata theory and its applications

This page was built for publication: Regular language representations in the constructive type theory of Coq