JEFL: joint embedding of formal proof libraries (Q831932): Difference between revisions

@@ Property / cites work @@
+Structured Formal Development with Quotient Types in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Matching Concepts across HOL Libraries
@@ Property / cites work: Matching Concepts across HOL Libraries / rank @@
+Normal rank
@@ Property / cites work @@
+Sharing HOL4 and HOL Light Proof Knowledge
@@ Property / cites work: Sharing HOL4 and HOL Light Proof Knowledge / rank @@
+Normal rank
@@ Property / cites work @@
+Aligning concepts across proof assistant libraries
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Light: An Overview
@@ Property / cites work: HOL Light: An Overview / 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 @@
+years of research and development around Coq
@@ Property / cites work: 30 years of research and development around Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Scalable LCF-Style Proof Translation
@@ Property / cites work: Scalable LCF-Style Proof Translation / rank @@
+Normal rank
@@ Property / cites work @@
+Lemma Mining over HOL Light
@@ Property / cites work: Lemma Mining over HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+HOL(y)Hammer: online ATP service for HOL Light
@@ Property / cites work: HOL(y)Hammer: online ATP service for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Importing HOL Light into Coq
@@ Property / cites work: Importing HOL Light into Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Recursive functions of symbolic expressions and their computation by machine, Part I
+Normal rank
@@ Property / cites work @@
+Classification of alignments between concepts of formal mathematical systems
+Normal rank
@@ Property / cites work @@
+The MMT API: A Generic MKM System
@@ Property / cites work: The MMT API: A Generic MKM System / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP World – Infrastructure for Automated Reasoning
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+Normal rank