A HOL Theorem Proving Interface for C
@inproceedings{TASE:CZF26,
author = {Cao, Yiyuan and Zhuang, Jiayi and Fan, Jinkai and Wang, Di and Hu, Zhenjiang},
booktitle = {Theor.\ Aspects of Softw.\ Eng.},
doi = {10.1145/3192366.3192408},
series = {TASE'26},
title = {{A HOL Theorem Proving Interface for C}},
year = {2026}
} Abstract
C programmers who wish to perform interactive theorem proving (e.g., when verifying critical code they write) currently face a language barrier: working with existing provers requires familiarity with their own proof languages—usually a custom tactic language or a functional programming language—far removed from the C programming environment and paradigm. To bridge this gap, we present the first higher-order logic (HOL) theorem proving interface for C. Our interface is comprehensive: it covers the core data types and operations of HOL theorem proving in the LCF style, readily usable for forward derivation of theorems by invoking existing inference rules. Our interface is trustworthy: by extending the LCF architecture with a client-server model, it ensures every theorem constructed by arbitrary C code is necessarily derived from a small trusted proof kernel. Finally, programming derived proof facilities in C is practical: we demonstrate this by implementing commonly used tactics for goal-directed reasoning as a library on top of our interface, which utilizes a goal-tree data structure dedicated to the bookkeeping of proof states and applies imperative programming patterns naturally.