Experiences from exporting major proof assistant libraries (Q2069875): Difference between revisions

@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Crafting a Proof Assistant
@@ Property / cites work: Crafting a Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Querying Proofs
@@ Property / cites work: Querying Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Translating the IMPS theory library to MMT/OMDoc
@@ Property / cites work: Translating the IMPS theory library to MMT/OMDoc / rank @@
+Normal rank
@@ Property / cites work @@
+Project Abstract: Logic Atlas and Integrator (LATIN)
+Normal rank
@@ Property / cites work @@
+Relational data across mathematical libraries
@@ Property / cites work: Relational data across mathematical libraries / rank @@
+Normal rank
@@ Property / cites work @@
+Hammer for Coq: automation for dependent type theory
+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 @@
+IMPS: An interactive mathematical proof system
@@ Property / cites work: IMPS: An interactive mathematical proof system / rank @@
+Normal rank
@@ Property / cites work @@
+Packaging Mathematical Structures
@@ Property / cites work: Packaging Mathematical Structures / rank @@
+Normal rank
@@ Property / cites work @@
+Aligning concepts across proof assistant libraries
+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 @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+The Mizar Mathematical Library in OMDoc: translation and applications
+Normal rank
@@ Property / cites work @@
+Scalable LCF-Style Proof Translation
@@ Property / cites work: Scalable LCF-Style Proof Translation / rank @@
+Normal rank
@@ Property / cites work @@
+Semantics of Mizar as an Isabelle object logic
@@ Property / cites work: Semantics of Mizar as an Isabelle object logic / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Knowledge Management for HOL Light
@@ Property / cites work: Towards Knowledge Management for HOL Light / rank @@
+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 @@
+Making PVS accessible to generic services by interpretation in a universal format
+Normal rank
@@ Property / cites work @@
+QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
+Normal rank
@@ Property / cites work @@
+A Mechanized Translation from Higher-Order Logic to Set Theory
+Normal rank
@@ Property / cites work @@
+Theories as types
@@ Property / cites work: Theories as types / rank @@
+Normal rank
@@ Property / cites work @@
+Representing structural language features in formal meta-languages
+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 @@
+Q4790669
@@ Property / cites work: Q4790669 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Capturing Hiproofs in HOL Light
@@ Property / cites work: Capturing Hiproofs in HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+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 @@
+A scalable module system
@@ Property / cites work: A scalable module system / rank @@
+Normal rank
@@ Property / cites work @@
+A Verified Theorem Prover Backend Supported by a Monotonic Library
+Normal rank
@@ Property / cites work @@
+A plugin to export Coq libraries to XML
@@ Property / cites work: A plugin to export Coq libraries to XML / rank @@
+Normal rank
@@ Property / cites work @@
+An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
+Normal rank
@@ Property / cites work @@
+Q4413895
@@ Property / cites work: Q4413895 / rank @@
+Normal rank