Effective interactive proofs for higher-order imperative programs

We present a new approach for constructing and verifying higherorder, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnit...

• Type: Conference
• Year: 2009
• Where: ICFP
• Authors: Adam J. Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky
• Keywords: Coq Proof Assistant, Data Structure Verification, ICFP 2009, Programming Languages, Reasonable Proof Burden