Proof Pearl: regular expression equivalence and relation algebra
From MaRDI portal
Publication:2392416
DOI10.1007/S10817-011-9223-4zbMATH Open1269.68090OpenAlexW1968602591MaRDI QIDQ2392416FDOQ2392416
Authors: Alexander Krauss, Tobias Nipkow 
Publication date: 1 August 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9223-4
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
- Certification of Termination Proofs Using CeTA
- Derivatives of Regular Expressions
- Title not available (Why is that?)
- A completeness theorem for Kleene algebras and the algebra of regular events
- An efficient Coq tactic for deciding Kleene algebras
- Code generation via higher-order rewrite systems
- A Decision Procedure for Bisimilarity of Generalized Regular Expressions
- Regular-expression derivatives re-examined
- Title not available (Why is that?)
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
- Title not available (Why is that?)
- 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
- Completeness theorems for Kleene algebra with tests and top
- Automated analysis of regular algebra
- 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
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)
