A verified proof checker for higher-order logic.

*(English)*Zbl 1433.68527Summary: We present a computer program for checking proofs in higher-order logic (HOL) that is verified to accept only valid proofs. The proof checker is defined as functions in HOL and synthesized to CakeML code, and uses the Candle theorem prover kernel to check logical inferences. The checker reads proofs in the OpenTheory article format, which means proofs produced by various HOL proof assistants are supported. The proof checker is implemented and verified using the HOL4 theorem prover, and comes with a proof of soundness.

##### MSC:

68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |

03B16 | Higher-order logic |

##### Software:

CakeML; HOL; HOL Light; HOL Zero; Isabelle/HOL; Jitawa; Milawa; MLton; OCaml; OpenTheory; Poly/ML; ProofPower
PDF
BibTeX
XML
Cite

\textit{O. Abrahamsson}, J. Log. Algebr. Methods Program. 112, Article ID 100530, 19 p. (2020; Zbl 1433.68527)

Full Text:
DOI

##### References:

[1] | Hurd, J., The OpenTheory standard theory library, (NFM (2011)), 177-191 |

[2] | Kumar, R.; Arthan, R.; Myreen, M. O.; Owens, S., Self-formalisation of higher-order logic - semantics, soundness, and a verified implementation, J. Autom. Reason., 56, 3, 221-259 (2016) |

[3] | Slind, K.; Norrish, M., A brief overview of HOL4, (TPHOLs (2008)), 28-32 |

[4] | Ho, S.; Abrahamsson, O.; Kumar, R.; Myreen, M. O.; Tan, Y. K.; Norrish, M., Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions, (IJCAR (2018)), 646-662 |

[5] | Tan, Y. K.; Myreen, M. O.; Kumar, R.; Fox, A.; Owens, S.; Norrish, M., The verified CakeML compiler backend, J. Funct. Program., 29, e2 (2019) |

[6] | Harrison, J., HOL Light: an overview, (TPHOLs (2009)), 60-66 |

[7] | Arthan, R., The ProofPower web pages [online] (2017), (Accessed 22 February 2019) |

[8] | Wadler, P., Monads for functional programming, (Advanced Functional Programming, Tutorial Text. Advanced Functional Programming, Tutorial Text, Lecture Notes in Computer Science (1995), Springer) |

[9] | Harrison, J., Towards self-verification of HOL Light, (IJCAR (2006)), 177-191 |

[10] | Milner, R.; Tofte, M.; Harper, R., Definition of Standard ML (1997), MIT Press |

[11] | Leroy, X.; Doligez, D.; Frisch, A.; Garrigue, J.; Rémy, D.; Vouillon, J., The OCaml system documentation and user’s manual [online] (2018), (Accessed 25 February 2019) |

[12] | Hurd, J., The OpenTheory article file format [online] (2014), (Accessed 22 February 2019) |

[13] | Guéneau, A.; Myreen, M. O.; Kumar, R.; Norrish, M., Verified characteristic formulae for CakeML, (ESOP (2017)), 584-610 |

[14] | Fox, A. C.J.; Myreen, M. O.; Tan, Y. K.; Kumar, R., Verified compilation of CakeML to multiple machine-code targets, (CPP (2017), ACM), 125-137 |

[15] | Fox, A. C.J., Directions in ISA specification, (ITP (2012), Springer), 338-344 |

[16] | Hurd, J., The OpenTheory tool [online] (2018), (Accessed 26 February 2019) |

[17] | The MLton compiler [online]. (Accessed 26 October 2019). |

[18] | The Poly/ML compiler [online]. (Accessed 26 October 2019). |

[19] | The Moscow ML compiler [online]. (Accessed 26 October 2019). |

[20] | Kumar, R.; Myreen, M. O.; Norrish, M.; Owens, S., CakeML: a verified implementation of ML, (POPL (2014)), 179-192 |

[21] | Adams, M., Introducing HOL Zero - (extended abstract), (ICMS (2010)), 142-143 |

[22] | Ridge, T.; Margetson, J., A mechanically verified, sound and complete theorem prover for first order logic, (TPHOLs (2005)), 294-309 |

[23] | Kaufmann, M.; Moore, J. S., An industrial strength theorem prover for a logic based on common lisp, IEEE Trans. Softw. Eng., 23, 4, 203-213 (1997) |

[24] | Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL - a Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer |

[25] | Davis, J.; Myreen, M. O., The reflective Milawa theorem prover is sound (down to the machine code that runs it), J. Autom. Reason., 55, 2, 117-183 (2015) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.