A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking
arXiv:2412.20973
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.
The paper was presented in the student session of the European Summer School in Logic, Language, and Information (ESSLLI) in 2016