Proof Pearl: regular expression equivalence and relation algebra
From MaRDI portal
Recommendations
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- A Compact Proof of Decidability for Regular Expression Equivalence
- A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Equivalence of regular expressions over a partially commutative alphabet
- scientific article; zbMATH DE number 762061
- An Equational Axiomatization of Bisimulation over Regular Expressions
- scientific article; zbMATH DE number 7774242
- scientific article; zbMATH DE number 3883630
- On regular expression proof complexity
Cites work
- A completeness theorem for Kleene algebras and the algebra of regular events
- A Decision Procedure for Bisimilarity of Generalized Regular Expressions
- An efficient Coq tactic for deciding Kleene algebras
- Certification of Termination Proofs Using CeTA
- Code generation via higher-order rewrite systems
- Derivatives of Regular Expressions
- scientific article; zbMATH DE number 1304993 (Why is no real title available?)
- scientific article; zbMATH DE number 2085164 (Why is no real title available?)
- Regular-expression derivatives re-examined
Cited in
(31)- 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
- On the fine-structure of regular algebra
- On regular expression proof complexity
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
- Unified decision procedures for regular expression equivalence
- Automated analysis of regular algebra
- Automated Reasoning in Higher-Order Regular Algebra
- Deciding regular expressions (in-)equivalence in Coq
- On completeness of omega-regular algebras
- Deciding synchronous Kleene algebra with derivatives
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- A formalisation of finite automata using hereditarily finite sets
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Completeness for identity-free Kleene lattices
- Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- POSIX lexing with derivatives of regular expressions
- Verified verifying: SMT-LIB for strings in Isabelle
- Pumping, with or without choice
- On tools for completeness of Kleene algebra with hypotheses
- Completeness theorems for Kleene algebra with tests and top
- Certainty in formalising SMT-LIB for strings in Isabelle
- Relations between equation automata and follow automata
- Diagrammatic algebra of first order logic
- Well-behaved (co)algebraic semantics of regular expressions in Dafny
- When Lawvere meets Peirce: an equational presentation of Boolean hyperdoctrines
- The calculus of neo-Peircean relations
- Building program construction and verification tools from algebraic principles
- Proving language inclusion and equivalence by coinduction
Describes a project that uses
Uses Software
This page was built for publication: Proof Pearl: regular expression equivalence and relation algebra
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2392416)
