An open framework for foundational proof-carrying code

• DOI: 10.1145/1190315.1190325
• Publication Date: 2007-04-05T19:41:00Z
• Authors: Xinyu Feng; Zhaozhong Ni; Zhong Shao; Yu Guo
• Keywords: Soundness; Proof assistant; Interoperation; Code (set theory); Proof of concept

Today's software systems often use many different computation features and span abstraction levels (e.g., user code runtime-system code). To build foundational certified systems, it is hard to have a single verification system supporting all features. In this paper we present an open framework for proof-carrying (FPCC). It allows program modules be specified separately using type or logics. Certified (i.e., proof) can linked together fully systems. The supports modular proof reuse. also expressive enough so that invariants established in specific are preserved even when they embedded into our framework. Our work presents the first FPCC systematically interoperation between mechanized Coq assistant with machine-checkable soundness proof.