A Verified Runtime for a Verified Theorem Prover (Q3088011): Difference between revisions

@@ Property / cites work @@
+Q4040283
@@ Property / cites work: Q4040283 / rank @@
+Normal rank
@@ Property / cites work @@
+A verified compiler for an impure functional language
+Normal rank
@@ Property / cites work @@
+Mechanized Verification of CPS Transformations
@@ Property / cites work: Mechanized Verification of CPS Transformations / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Q4838159
@@ Property / cites work: Q4838159 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247076
@@ Property / cites work: Q4247076 / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Self-verification of HOL Light
@@ Property / cites work: Towards Self-verification of HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Light: An Overview
@@ Property / cites work: HOL Light: An Overview / rank @@
+Normal rank
@@ Property / cites work @@
+Formal certification of a compiler back-end or
@@ Property / cites work: Formal certification of a compiler back-end or / rank @@
+Normal rank
@@ Property / cites work @@
+Recursive functions of symbolic expressions and their computation by machine, Part I
+Normal rank
@@ Property / cites work @@
+A certified framework for compiling and executing garbage-collected languages
+Normal rank
@@ Property / cites work @@
+Verified just-in-time compiler on x86
@@ Property / cites work: Verified just-in-time compiler on x86 / 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 @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank