2024/12/30 by Shuai Wang, Wang, Shuai
Computer Science · #Security and Verification in Computing #Software Testing and Debugging Techniques #Parallel Computing and Optimization Techniques
paper · pdf · doi:10.48550/arxiv.2412.20973
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.