Verified decision procedures for MSO on words based on derivatives of regular expressions
From MaRDI portal
Publication:5371957
DOI10.1017/S0956796815000246zbMath1420.68049MaRDI QIDQ5371957
Dmitriy Traytel, Tobias Nipkow
Publication date: 23 October 2017
Published in: Journal of Functional Programming (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Partial derivatives of regular expressions and finite automaton constructions
- Isabelle/HOL. A proof assistant for higher-order logic
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- Proof Pearl: regular expression equivalence and relation algebra
- The dual of concatenation
- Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
- Unified Decision Procedures for Regular Expression Equivalence
- A Compact Proof of Decidability for Regular Expression Equivalence
- Deciding Regular Expressions (In-)Equivalence in Coq
- Concrete Semantics
- Checking NFA equivalence with bisimulations up to congruence
- Partial Derivatives of an Extended Regular Expression
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Formalizing the Logic-Automaton Connection
- Code Generation via Higher-Order Rewrite Systems
- Regular-expression derivatives re-examined
- Total parser combinators
- A play on regular expressions
- Parsing with derivatives
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Data Refinement in Isabelle/HOL
- A Procedure for Checking Equality of Regular Expressions
- Derivatives of Regular Expressions
- An Efficient Coq Tactic for Deciding Kleene Algebras
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
This page was built for publication: Verified decision procedures for MSO on words based on derivatives of regular expressions
