Introduction to ``Milestones in interactive theorem proving'' (Q1663212): Difference between revisions

@@ Property / cites work @@
+Verified software: Theories, tools, experiments. Second international conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings
+Normal rank
@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736387
@@ Property / cites work: Q4736387 / rank @@
+Normal rank
@@ Property / cites work @@
+Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+A verified compiler from Isabelle/HOL to CakeML
@@ Property / cites work: A verified compiler from Isabelle/HOL to CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+Unification in Boolean rings
@@ Property / cites work: Unification in Boolean rings / rank @@
+Normal rank
@@ Property / cites work @@
+Boolean unification - the story so far
@@ Property / cites work: Boolean unification - the story so far / rank @@
+Normal rank
@@ Property / cites work @@
+A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
+Normal rank
@@ Property / cites work @@
+Equational reasoning in Isabelle
@@ Property / cites work: Equational reasoning in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Term rewriting and beyond -- theorem proving in Isabelle
+Normal rank
@@ Property / cites work @@
+Unification in primal algebras, their powers and their varieties
+Normal rank
@@ Property / cites work @@
+Higher-order unification, polymorphism, and subsorts
+Normal rank
@@ Property / cites work @@
+Winskel is (almost) right: Towards a mechanized semantics textbook
+Normal rank
@@ Property / cites work @@
+Q2769440
@@ Property / cites work: Q2769440 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4435474
@@ Property / cites work: Q4435474 / rank @@
+Normal rank
@@ Property / cites work @@
+Linear quantifier elimination
@@ Property / cites work: Linear quantifier elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Flyspeck I: Tame Graphs
@@ Property / cites work: Flyspeck I: Tame Graphs / rank @@
+Normal rank
@@ Property / cites work @@
+Concrete Semantics
@@ Property / cites work: Concrete Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Modular higher-order E-unification
@@ Property / cites work: Modular higher-order E-unification / rank @@
+Normal rank
@@ Property / cites work @@
+Q3956381
@@ Property / cites work: Q3956381 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic for Programming, Artificial Intelligence, and Reasoning
+Normal rank
@@ Property / cites work @@
+Hoare logic for Java in Isabelle/HOL
@@ Property / cites work: Hoare logic for Java in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8--13, 2012. Proceedings
+Normal rank