Cited in
(23)- Verified decision procedures for MSO on words based on derivatives of regular expressions
- A Mechanized Proof of Higman’s Lemma by Open Induction
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- Two-Way Automata in Coq
- Formally verified algorithms for upper-bounding state space diameters
- Regular language representations in the constructive type theory of Coq
- Automated Reasoning in Higher-Order Regular Algebra
- A Verified Compositional Algorithm for AI Planning
- On the fine-structure of regular algebra
- Gauss Jordan Elimination
- Presburger Automata
- Regular Sets
- Finite Automata HF
- Hotel Key Card
- Hereditarily Finite Sets
- Decreasing Diagrams II
- Well Quasi Orders
- Worker/Wrapper Transformation
- MSO_Regex_Equivalence
- Regex_Equivalence
- A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
- Open Induction
- A Decision Procedure for Regular Expression Equivalence in Type Theory
This page was built for software: Myhill-Nerode
