Deciding Regular Expressions (In-)Equivalence in Coq (Q2915138): Difference between revisions

@@ Property / describes a project that uses @@
+PDCoq
@@ Property / describes a project that uses: PDCoq / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-33314-9_7
+Normal rank
@@ Property / OpenAlex ID @@
+W69247107
@@ Property / OpenAlex ID: W69247107 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Automated Reasoning in Kleene Algebra
@@ Property / cites work: Automated Reasoning in Kleene Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Q4362921
@@ Property / cites work: Q4362921 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial Derivative Automata Formalized in Coq
@@ Property / cites work: Partial Derivative Automata Formalized in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+ANTIMIROV AND MOSSES'S REWRITE SYSTEM REVISITED
@@ Property / cites work: ANTIMIROV AND MOSSES'S REWRITE SYSTEM REVISITED / rank @@
+Normal rank
@@ Property / cites work @@
+Rewriting extended regular expressions
@@ Property / cites work: Rewriting extended regular expressions / rank @@
+Normal rank
@@ Property / cites work @@
+Q2819377
@@ Property / cites work: Q2819377 / rank @@
+Normal rank
@@ Property / cites work @@
+The Average Transition Complexity of Glushkov and Partial Derivative Automata
+Normal rank
@@ Property / cites work @@
+An Efficient Coq Tactic for Deciding Kleene Algebras
+Normal rank
@@ Property / cites work @@
+A completeness theorem for Kleene algebras and the algebra of regular events
+Normal rank
@@ Property / cites work @@
+A Decision Procedure for Regular Expression Equivalence in Type Theory
+Normal rank
@@ Property / cites work @@
+Derivatives of Regular Expressions
@@ Property / cites work: Derivatives of Regular Expressions / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Pearl: regular expression equivalence and relation algebra
+Normal rank
@@ Property / cites work @@
+Q4251915
@@ Property / cites work: Q4251915 / rank @@
+Normal rank
@@ Property / cites work @@
+A Compact Proof of Decidability for Regular Expression Equivalence
+Normal rank
@@ Property / cites work @@
+Deciding Kleene algebra terms equivalence in Coq
@@ Property / cites work: Deciding Kleene algebra terms equivalence in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q4506483
@@ Property / cites work: Q4506483 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2711324
@@ Property / cites work: Q2711324 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281483
@@ Property / cites work: Q4281483 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4484330
@@ Property / cites work: Q4484330 / rank @@
+Normal rank
@@ Property / cites work @@
+On Hoare logic and Kleene algebra with tests
@@ Property / cites work: On Hoare logic and Kleene algebra with tests / rank @@
+Normal rank