Deep Generation of Coq Lemma Names Using Elaborated Terms (Q5048996): Difference between revisions

@@ Property / describes a project that uses @@
+Adam
@@ Property / describes a project that uses: Adam / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PyTorch
@@ Property / describes a project that uses: PyTorch / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+JSNice
@@ Property / describes a project that uses: JSNice / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HoTT
@@ Property / describes a project that uses: HoTT / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3046547863
@@ Property / OpenAlex ID: W3046547863 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
+Normal rank
@@ Property / cites work @@
+What’s in a Theorem Name?
@@ Property / cites work: What’s in a Theorem Name? / rank @@
+Normal rank
@@ Property / cites work @@
+Autarkic computations in formal proofs
@@ Property / cites work: Autarkic computations in formal proofs / rank @@
+Normal rank
@@ Property / cites work @@
+A Formal Library for Elliptic Curves in the Coq Proof Assistant
+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 @@
+Mining the Archive of Formal Proofs
@@ Property / cites work: Mining the Archive of Formal Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q2767010
@@ Property / cites work: Q2767010 / rank @@
+Normal rank
@@ Property / cites work @@
+Regular language representations in the constructive type theory of Coq
+Normal rank
@@ Property / cites work @@
+Q5302559
@@ Property / cites work: Q5302559 / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+ML4PG in Computer Algebra Verification
@@ Property / cites work: ML4PG in Computer Algebra Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Recycling proof patterns in Coq: case studies
@@ Property / cites work: Recycling proof patterns in Coq: case studies / rank @@
+Normal rank
@@ Property / cites work @@
+Recursive functions of symbolic expressions and their computation by machine, Part I
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+Normal rank
@@ Property / cites work @@
+The Coq library as a theory graph
@@ Property / cites work: The Coq library as a theory graph / rank @@
+Normal rank
@@ Property / cites work @@
+Predicting Program Properties from "Big Code"
@@ Property / cites work: Predicting Program Properties from "Big Code" / rank @@
+Normal rank