Cited in
(22)- Verified decision procedures for MSO on words based on derivatives of regular expressions
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- Two-Way Automata in Coq
- Regular language representations in the constructive type theory of Coq
- Verified synthesis of knowledge-based programs in finite synchronous environments
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- MCK
- CAVA Automata Library
- Depth First Search
- Gauss Jordan Elimination
- KBPs
- Myhill-Nerode
- Regular Sets
- Finite Automata HF
- Hereditarily Finite Sets
- LTL_to_GBA
- Real_Impl
- Tree Automata
- MSO_Regex_Equivalence
- Regex_Equivalence
- Automatic refinement to efficient data structures: a comparison of two approaches
- Partial and nested recursive function definitions in higher-order logic
This page was built for software: Presburger Automata
