A Decision Procedure for Regular Expression Equivalence in Type Theory
From MaRDI portal
Publication:3100207
DOI10.1007/978-3-642-25379-9_11zbMATH Open1350.68228OpenAlexW2235749104MaRDI QIDQ3100207FDOQ3100207
Authors: Thierry Coquand, Vincent Siles 
Publication date: 22 November 2011
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_11
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
- Certification of Termination Proofs Using CeTA
- Derivatives of Regular Expressions
- Title not available (Why is that?)
- An introduction to small scale reflection in Coq
- Weak Second‐Order Arithmetic and Finite Automata
- Proof Pearl: regular expression equivalence and relation algebra
- An efficient Coq tactic for deciding Kleene algebras
- Well quasi-ordered sets
- Terminating general recursion
- Regular-expression derivatives re-examined
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- Partial derivative automata formalized in Coq
- On streams that are finitely red
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
- Proof Pearl: regular expression equivalence and relation algebra
- Proving language inclusion and equivalence by coinduction
- 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
Uses Software
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)
