A verified proof checker for higher-order logic

DOI10.1016/j.jlamp.2020.100530zbMath1433.68527OpenAlexW3007423032MaRDI QIDQ1987736

Oskar Abrahamsson

Publication date: 15 April 2020

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2020.100530

zbMATH Keywords

higher-order logicsoundnessproof checkermechanized proof

Mathematics Subject Classification ID

Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

\texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Isabelle's metalogic: formalization and proof checker ⋮ A formalization and proof checker for Isabelle's metalogic

Uses Software

• Isabelle/HOL
• HOL
• ProofPower
• OCaml
• HOL Light
• CakeML
• Milawa
• Poly/ML
• Jitawa
• MLton
• HOL Zero
• OpenTheory

Cites Work

• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
• Verified Characteristic Formulae for CakeML
• HOL Light: An Overview
• A Brief Overview of HOL4
• Towards Self-verification of HOL Light
• The verified CakeML compiler backend
• CakeML
• Theorem Proving in Higher Order Logics

This page was built for publication: A verified proof checker for higher-order logic