A Decision Procedure for Regular Expression Equivalence in Type Theory
From MaRDI portal
Publication:3100207
Recommendations
- A Compact Proof of Decidability for Regular Expression Equivalence
- A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
- Unified decision procedures for regular expression equivalence
- Deciding regular expressions (in-)equivalence in Coq
- Publication:4943321
- Programming Languages and Systems
- Deciding definability by deterministic regular expressions
- Deciding definability by deterministic regular expressions
- Regular expression containment, coinductive axiomatization and computational interpretation
- scientific article; zbMATH DE number 4068831
Cites work
- scientific article; zbMATH DE number 3574077 (Why is no real title available?)
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- An efficient Coq tactic for deciding Kleene algebras
- An introduction to small scale reflection in Coq
- Certification of Termination Proofs Using CeTA
- Derivatives of Regular Expressions
- On streams that are finitely red
- Partial derivative automata formalized in Coq
- Proof Pearl: regular expression equivalence and relation algebra
- Regular-expression derivatives re-examined
- Terminating general recursion
- Weak Second‐Order Arithmetic and Finite Automata
- Well quasi-ordered sets
Cited in
(18)- A constructive theory of regular languages in Coq
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- Deciding synchronous Kleene algebra with derivatives
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
- POSIX lexing with derivatives of regular expressions
- A Decision Procedure for Bisimilarity of Generalized Regular Expressions
- Regular language representations in the constructive type theory of Coq
- A Compact Proof of Decidability for Regular Expression Equivalence
- Proving language inclusion and equivalence by coinduction
- Proof Pearl: regular expression equivalence and relation algebra
- Types for Proofs and Programs
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Deciding Kleene algebra terms equivalence in Coq
- Deciding regular expressions (in-)equivalence in Coq
- Two-Way Automata in Coq
- ANTIMIROV AND MOSSES'S REWRITE SYSTEM REVISITED
- Pumping, with or without choice
- Unified decision procedures for regular expression equivalence
This page was built for publication: A Decision Procedure for Regular Expression Equivalence in Type Theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100207)
