swMATH28793MaRDI QIDQ40507FDOQ40507
Author name not available (Why is that?)
Official website: https://www.isa-afp.org/entries/Regular-Sets.html
Cited In (33)
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- On completeness of omega-regular algebras
- Title not available (Why is that?)
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Building program construction and verification tools from algebraic principles
- Regular language representations in the constructive type theory of Coq
- KAT-ML
- RALL
- FAdo
- GUItar
- PDCoq
- NetKAT
- Proof Pearl: regular expression equivalence and relation algebra
- Proving language inclusion and equivalence by coinduction
- AmiCo
- Gauss Jordan Elimination
- Myhill-Nerode
- POSIX Lexing
- Presburger Automata
- Finite Automata HF
- Hereditarily Finite Sets
- Worker/Wrapper Transformation
- MSO_Regex_Equivalence
- Regex_Equivalence
- Simpl
- 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
- Completeness for identity-free Kleene lattices
- Deciding Kleene algebras in \texttt{Coq}
- Automated Reasoning in Higher-Order Regular Algebra
This page was built for software: Regular Sets
