A formalisation of the Myhill-Nerode theorem based on regular expressions
From MaRDI portal
Publication:2351151
DOI10.1007/s10817-013-9297-2zbMath1314.68179OpenAlexW2054695370MaRDI QIDQ2351151
Xing-Yuan Zhang, Christian Urban, Chunhan Wu
Publication date: 23 June 2015
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-013-9297-2
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
A Formalisation of Finite Automata Using Hereditarily Finite Sets ⋮ Regular language representations in the constructive type theory of Coq ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ A Mechanized Proof of Higman’s Lemma by Open Induction ⋮ Myhill-Nerode ⋮ Two-Way Automata in Coq ⋮ On the fine-structure of regular algebra
Uses Software
Cites Work
- Partial derivatives of regular expressions and finite automaton constructions
- The complexity of finding SUBSEQ\((A)\)
- Adapting functional programs to higher order logic
- Proof Pearl: regular expression equivalence and relation algebra
- Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
- A Compact Proof of Decidability for Regular Expression Equivalence
- A Constructive Theory of Regular Languages in Coq
- Certified Kruskal’s Tree Theorem
- Succinctness of the Complement and Intersection of Regular Expressions
- Partial Derivative Automata Formalized in Coq
- A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Formalizing the Logic-Automaton Connection
- EDUCATIONAL PEARL: ‘Proof-directed debugging’ revisited for a first-order version
- A Second Course in Formal Languages and Automata Theory
- Regular-expression derivatives re-examined
- Proof-directed debugging
- On free monoids partially ordered by embedding
- Derivatives of Regular Expressions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A formalisation of the Myhill-Nerode theorem based on regular expressions
