Regular Sets
From MaRDI portal
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
- scientific article; zbMATH DE number 7533344 (Why is no real title available?)
- 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
- KAT-ML
- RALL
- 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
- Regular language representations in the constructive type theory of Coq
- Proving language inclusion and equivalence by coinduction
- Proof Pearl: regular expression equivalence and relation algebra
- 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