Verified decision procedures for MSO on words based on derivatives of regular expressions (Q5371957): Difference between revisions

@@ Property / describes a project that uses @@
+Regex_Equivalence
@@ Property / describes a project that uses: Regex_Equivalence / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Myhill-Nerode
@@ Property / describes a project that uses: Myhill-Nerode / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Partial derivatives of regular expressions and finite automaton constructions
+Normal rank
@@ Property / cites work @@
+A Compact Proof of Decidability for Regular Expression Equivalence
+Normal rank
@@ Property / cites work @@
+Q2754076
@@ Property / cites work: Q2754076 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpretation of Locales in Isabelle: Theories and Proof Contexts
+Normal rank
@@ Property / cites work @@
+Q2782479
@@ Property / cites work: Q2782479 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing the Logic-Automaton Connection
@@ Property / cites work: Formalizing the Logic-Automaton Connection / rank @@
+Normal rank
@@ Property / cites work @@
+Checking NFA equivalence with bisimulations up to congruence
+Normal rank
@@ Property / cites work @@
+An Efficient Coq Tactic for Deciding Kleene Algebras
+Normal rank
@@ Property / cites work @@
+Derivatives of Regular Expressions
@@ Property / cites work: Derivatives of Regular Expressions / rank @@
+Normal rank
@@ Property / cites work @@
+Partial Derivatives of an Extended Regular Expression
+Normal rank
@@ Property / cites work @@
+A Decision Procedure for Regular Expression Equivalence in Type Theory
+Normal rank
@@ Property / cites work @@
+Total parser combinators
@@ Property / cites work: Total parser combinators / rank @@
+Normal rank
@@ Property / cites work @@
+A play on regular expressions
@@ Property / cites work: A play on regular expressions / rank @@
+Normal rank
@@ Property / cites work @@
+A Procedure for Checking Equality of Regular Expressions
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Data Refinement in Isabelle/HOL
@@ Property / cites work: Data Refinement in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Q4818808
@@ Property / cites work: Q4818808 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Pearl: regular expression equivalence and relation algebra
+Normal rank
@@ Property / cites work @@
+Parsing with derivatives
@@ Property / cites work: Parsing with derivatives / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding Regular Expressions (In-)Equivalence in Coq
+Normal rank
@@ Property / cites work @@
+Concrete Semantics
@@ Property / cites work: Concrete Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Unified Decision Procedures for Regular Expression Equivalence
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+The dual of concatenation
@@ Property / cites work: The dual of concatenation / rank @@
+Normal rank
@@ Property / cites work @@
+Regular-expression derivatives re-examined
@@ Property / cites work: Regular-expression derivatives re-examined / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754118
@@ Property / cites work: Q2754118 / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
+Normal rank
@@ Property / cites work @@
+Q4251915
@@ Property / cites work: Q4251915 / rank @@
+Normal rank
@@ Property / cites work @@
+Verified decision procedures for MSO on words based on derivatives of regular expressions
+Normal rank
@@ Property / cites work @@
+A formalisation of the Myhill-Nerode theorem based on regular expressions
+Normal rank