Regular Sets
From MaRDI portal
Cited in
(33)- Regular language representations in the constructive type theory of Coq
- RALL
- KAT-ML
- FAdo
- GUItar
- PDCoq
- Deciding Kleene algebra terms equivalence in Coq
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- Proof Pearl: regular expression equivalence and relation algebra
- NetKAT
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
- Deciding Kleene algebras in \texttt{Coq}
- Automated Reasoning in Higher-Order Regular Algebra
- Deciding regular expressions (in-)equivalence in Coq
- On completeness of omega-regular algebras
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- AmiCo
- Myhill-Nerode
- POSIX Lexing
- Presburger Automata
- Gauss Jordan Elimination
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Hereditarily Finite Sets
- Finite Automata HF
- Worker/Wrapper Transformation
- Regex_Equivalence
- MSO_Regex_Equivalence
- Simpl
- Completeness for identity-free Kleene lattices
- Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Building program construction and verification tools from algebraic principles
- Proving language inclusion and equivalence by coinduction
This page was built for software: Regular Sets
