Generating certified code from formal proofs: a case study in homological algebra (Q968307): Difference between revisions

@@ Property / cites work @@
+Artificial Intelligence and Symbolic Computation
@@ Property / cites work: Artificial Intelligence and Symbolic Computation / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Systems Theory – EUROCAST 2005
@@ Property / cites work: Computer Aided Systems Theory – EUROCAST 2005 / rank @@
+Normal rank
@@ Property / cites work @@
+A mechanized proof of the basic perturbation lemma
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Interpretation of Locales in Isabelle: Theories and Proof Contexts
+Normal rank
@@ Property / cites work @@
+Q4435458
@@ Property / cites work: Q4435458 / rank @@
+Normal rank
@@ Property / cites work @@
+A Fixed Point Approach to Homological Perturbation Theory
+Normal rank
@@ Property / cites work @@
+Towards Constructive Homological Algebra in Type Theory
+Normal rank
@@ Property / cites work @@
+Object oriented institutions to specify symbolic computation systems
+Normal rank
@@ Property / cites work @@
+A Modular Formalisation of Finite Group Theory
@@ Property / cites work: A Modular Formalisation of Finite Group Theory / rank @@
+Normal rank
@@ Property / cites work @@
+On the chain-complex of a fibration
@@ Property / cites work: On the chain-complex of a fibration / rank @@
+Normal rank
@@ Property / cites work @@
+A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
+Normal rank
@@ Property / cites work @@
+An object-oriented interpretation of the EAT system
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q4247084
@@ Property / cites work: Q4247084 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Pearl: Looping Around the Orbit
@@ Property / cites work: Proof Pearl: Looping Around the Orbit / rank @@
+Normal rank
@@ Property / cites work @@
+Flyspeck II: The basic linear programs
@@ Property / cites work: Flyspeck II: The basic linear programs / rank @@
+Normal rank
@@ Property / cites work @@
+Adapting functional programs to higher order logic
+Normal rank