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

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Regular Sets
@@ Property / describes a project that uses: Regular Sets / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CeTA
@@ Property / describes a project that uses: CeTA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq/SSReflect
@@ Property / describes a project that uses: Coq/SSReflect / 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 / full work available at URL @@
+https://doi.org/10.1007/978-3-642-25379-9_11
+Normal rank
@@ Property / OpenAlex ID @@
+W2235749104
@@ Property / OpenAlex ID: W2235749104 / 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 @@
+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