Cited in
(33)- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Deciding Kleene algebras in \texttt{Coq}
- Regular language representations in the constructive type theory of Coq
- Automated Reasoning in Higher-Order Regular Algebra
- Building program construction and verification tools from algebraic principles
- Deciding regular expressions (in-)equivalence in Coq
- Proof Pearl: regular expression equivalence and relation algebra
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- scientific article; zbMATH DE number 7533344 (Why is no real title available?)
- KAT-ML
- RALL
- Proving language inclusion and equivalence by coinduction
- FAdo
- GUItar
- PDCoq
- NetKAT
- 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
- Deciding Kleene algebra terms equivalence in Coq
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
- On completeness of omega-regular algebras
- Completeness for identity-free Kleene lattices
This page was built for software: Regular Sets
