Regular language representations in the constructive type theory of Coq

DOI10.1007/S10817-018-9460-XMaRDI QIDQ1663246zbMATH OpenOpenAlexWikidataFDO

Authors Christian Doczkal, Gert Smolka

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

Coqinteractive theorem provingregular languagesWS1Sconstructive type theorytwo-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)

Recommendations

• A constructive theory of regular languages in Coq
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Deciding regular expressions (in-)equivalence in Coq
• Partial derivative automata formalized in Coq
• Two-Way Automata in Coq

Cites work

• scientific article; zbMATH DE number 1033559 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• 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 formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• A note on the reduction of two-way automata to one-way automata
• Automata theory and its applications
• Automatentheorie und Logik
• Deciding Kleene algebra terms equivalence in Coq
• Deciding Kleene algebras in \texttt{Coq}
• Decision Problems of Finite Automata Design and Related Arithmetics
• Derivatives of Regular Expressions
• Endmarkers can make a difference
• Explicit substitutions
• Formalizing the Logic-Automaton Connection
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• Kleene algebra with tests and Coq tools for while programs
• Pragmatic quotient types in Coq
• Proof Pearl: regular expression equivalence and relation algebra
• Structural analysis of narratives with the Coq proof assistant
• Succinctness of the Complement and Intersection of Regular Expressions
• The Complexity of Translating Logic to Finite Automata
• Two-Way Automata in Coq
• Two-way finite automata: old and recent results
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(7)

• Partial derivative automata formalized in Coq
• A mechanized theory of regular trees in dependent type theory
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• A constructive theory of regular languages in Coq
• Encoding natural semantics in Coq
• Pumping, with or without choice
• Deep Generation of Coq Lemma Names Using Elaborated Terms

Describes a project that uses

Uses Software

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

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)