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

@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+NQTHM
@@ Property / describes a project that uses: NQTHM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Milawa
@@ Property / describes a project that uses: Milawa / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GCminor
@@ Property / describes a project that uses: GCminor / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OCaml
@@ Property / describes a project that uses: OCaml / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-22863-6_20
+Normal rank
@@ Property / OpenAlex ID @@
+W2216239550
@@ Property / OpenAlex ID: W2216239550 / rank @@
+Normal rank
@@ 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