Deciding Regular Expressions (In-)Equivalence in Coq

DOI10.1007/978-3-642-33314-9_7zbMath1330.68265OpenAlexW69247107MaRDI QIDQ2915138

David P. Pereira, Simão Melo de Sousa, Nelma Moreira

Publication date: 21 September 2012

Published in: Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Deciding Synchronous Kleene Algebra with Derivatives ⋮ Proving language inclusion and equivalence by coinduction ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Deciding Kleene algebra terms equivalence in Coq

Uses Software

• Coq
• Prover9
• Mace4
• Coq/SSReflect
• FAdo
• GUItar
• PDCoq
• Regular Sets

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rewriting extended regular expressions
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A completeness theorem for Kleene algebras and the algebra of regular events
• Deciding Kleene algebra terms equivalence in Coq
• Proof Pearl: regular expression equivalence and relation algebra
• A Compact Proof of Decidability for Regular Expression Equivalence
• Partial Derivative Automata Formalized in Coq
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• ANTIMIROV AND MOSSES'S REWRITE SYSTEM REVISITED
• Automated Reasoning in Kleene Algebra
• The Average Transition Complexity of Glushkov and Partial Derivative Automata
• Derivatives of Regular Expressions
• On Hoare logic and Kleene algebra with tests
• An Efficient Coq Tactic for Deciding Kleene Algebras