Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking

Shuai Wang

TL;DR

The paper tackles reliability and efficiency in proof checking for higher-order logic by introducing HOLALA, a HOL Light variant that extends the kernel to make $\rightarrow$ and $\forall$ primitive and by embedding proofs into Dedukti via Holide. The core finding is that such kernel extension markedly shortens proofs (to roughly 64% of the original size) and speeds up proof checking (by about 38–41%), without compromising soundness. This suggests that a larger, carefully designed kernel can improve verification performance, motivating further exploration of additional primitives and cross-system evaluations (e.g., with HOL4). The work demonstrates a practical pathway to balance kernel size, proof length, and checking speed in interactive theorem proving.

Abstract

For the sake of reliability, the kernels of Interactive Theorem Provers (ITPs) are generally kept relatively small. On top of the kernel, additional symbols and inference rules are defined. This paper presents an analysis of how kernel extension reduces the size of proofs and impacts proof checking.

A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking

TL;DR

The paper tackles reliability and efficiency in proof checking for higher-order logic by introducing HOLALA, a HOL Light variant that extends the kernel to make and primitive and by embedding proofs into Dedukti via Holide. The core finding is that such kernel extension markedly shortens proofs (to roughly 64% of the original size) and speeds up proof checking (by about 38–41%), without compromising soundness. This suggests that a larger, carefully designed kernel can improve verification performance, motivating further exploration of additional primitives and cross-system evaluations (e.g., with HOL4). The work demonstrates a practical pathway to balance kernel size, proof length, and checking speed in interactive theorem proving.

Abstract

For the sake of reliability, the kernels of Interactive Theorem Provers (ITPs) are generally kept relatively small. On top of the kernel, additional symbols and inference rules are defined. This paper presents an analysis of how kernel extension reduces the size of proofs and impacts proof checking.
Paper Structure (8 sections, 1 figure, 3 tables)

This paper contains 8 sections, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. HOL Light
  3. Kernel Extension
  4. Proof Checking and Evaluation
  5. Extending Holide and Dedukti
  6. Evaluation
  7. Conclusion and Discussion
  8. Acknowledgement

Figures (1)

  • Figure 1: Dependency Analysis