Proof Pearl: regular expression equivalence and relation algebra
From MaRDI portal
Publication:2392416
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
- scientific article; zbMATH DE number 1304993 (Why is no real title available?)
- scientific article; zbMATH DE number 2085164 (Why is no real title available?)
- A Decision Procedure for Bisimilarity of Generalized Regular Expressions
- A completeness theorem for Kleene algebras and the algebra of regular events
- 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
- Regular-expression derivatives re-examined
Cited in
(25)- A Decision Procedure for Regular Expression Equivalence in Type Theory
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- On the fine-structure of regular algebra
- On completeness of omega-regular algebras
- scientific article; zbMATH DE number 7533344 (Why is no real title available?)
- Deciding synchronous Kleene algebra with derivatives
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
- POSIX lexing with derivatives of regular expressions
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Building program construction and verification tools from algebraic principles
- On tools for completeness of Kleene algebra with hypotheses
- Regular language representations in the constructive type theory of Coq
- Proving language inclusion and equivalence by coinduction
- Verified verifying: SMT-LIB for strings in Isabelle
- Automated analysis of regular algebra
- Completeness theorems for Kleene algebra with tests and top
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- On regular expression proof complexity
- Deciding Kleene algebra terms equivalence in Coq
- Deciding regular expressions (in-)equivalence in Coq
- Completeness for identity-free Kleene lattices
- Pumping, with or without choice
- Automated Reasoning in Higher-Order Regular Algebra
- Unified decision procedures for regular expression equivalence
- A formalisation of finite automata using hereditarily finite sets
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)
