A verified proof checker for higher-order logic (Q1987736): Difference between revisions

@@ Property / DOI @@
-.1016/j.jlamp.2020.100530
@@ Property / DOI: 10.1016/j.jlamp.2020.100530 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OCaml
@@ Property / describes a project that uses: OCaml / 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 @@
+Poly/ML
@@ Property / describes a project that uses: Poly/ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MLton
@@ Property / describes a project that uses: MLton / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ProofPower
@@ Property / describes a project that uses: ProofPower / 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 @@
+Jitawa
@@ Property / describes a project that uses: Jitawa / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Zero
@@ Property / describes a project that uses: HOL Zero / 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.1016/j.jlamp.2020.100530
+Normal rank
@@ Property / OpenAlex ID @@
+W3007423032
@@ Property / OpenAlex ID: W3007423032 / rank @@
+Normal rank
@@ Property / cites work @@
+Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
+Normal rank
@@ Property / cites work @@
+The verified CakeML compiler backend
@@ Property / cites work: The verified CakeML compiler backend / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Light: An Overview
@@ Property / cites work: HOL Light: An Overview / 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 @@
+Verified Characteristic Formulae for CakeML
@@ Property / cites work: Verified Characteristic Formulae for CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+CakeML
@@ Property / cites work: CakeML / 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 @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+The reflective Milawa theorem prover is sound (down to the machine code that runs it)
+Normal rank
@@ Property / DOI @@
+.1016/J.JLAMP.2020.100530
@@ Property / DOI: 10.1016/J.JLAMP.2020.100530 / rank @@
+Normal rank