A Decision Procedure for Regular Expression Equivalence in Type Theory

DOI10.1007/978-3-642-25379-9_11zbMath1350.68228MaRDI QIDQ3100207

Thierry Coquand, Vincent Siles

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_11

Mathematics Subject Classification ID

Related Items

Verified decision procedures for MSO on words based on derivatives of regular expressions, Proving language inclusion and equivalence by coinduction, Regular language representations in the constructive type theory of Coq, Deciding Kleene algebra terms equivalence in Coq, A formalisation of the Myhill-Nerode theorem based on regular expressions, POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl), Two-Way Automata in Coq, Deciding Regular Expressions (In-)Equivalence in Coq, Deciding Synchronous Kleene Algebra with Derivatives

Uses Software

• Coq
• CeTA
• Coq/SSReflect
• Myhill-Nerode
• Regular Sets

Cites Work

• Unnamed Item
• Unnamed Item
• Terminating general recursion
• Well quasi-ordered sets
• Proof Pearl: regular expression equivalence and relation algebra
• Partial Derivative Automata Formalized in Coq
• A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
• On streams that are finitely red
• Certification of Termination Proofs Using CeTA
• Weak Second‐Order Arithmetic and Finite Automata
• Regular-expression derivatives re-examined
• Derivatives of Regular Expressions
• An Efficient Coq Tactic for Deciding Kleene Algebras