A Decision Procedure for Regular Expression Equivalence in Type Theory

DOI10.1007/978-3-642-25379-9_11zbMath1350.68228OpenAlexW2235749104MaRDI 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 (10)

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

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

This page was built for publication: A Decision Procedure for Regular Expression Equivalence in Type Theory