A Decision Procedure for Regular Expression Equivalence in Type Theory (Q3100207): Difference between revisions

@@ Property / cites work @@
+Partial Derivative Automata Formalized in Coq
@@ Property / cites work: Partial Derivative Automata Formalized in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+On streams that are finitely red
@@ Property / cites work: On streams that are finitely red / rank @@
+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 @@
+Weak Second‐Order Arithmetic and Finite Automata
+Normal rank
@@ Property / cites work @@
+Q4145861
@@ Property / cites work: Q4145861 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Pearl: regular expression equivalence and relation algebra
+Normal rank
@@ Property / cites work @@
+Terminating general recursion
@@ Property / cites work: Terminating general recursion / 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 @@
+Well quasi-ordered sets
@@ Property / cites work: Well quasi-ordered sets / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075246
@@ Property / cites work: Q3075246 / rank @@
+Normal rank
@@ Property / cites work @@
+Certification of Termination Proofs Using CeTA
@@ Property / cites work: Certification of Termination Proofs Using CeTA / rank @@
+Normal rank
@@ Property / cites work @@
+A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
+Normal rank