Date Added: Sep 2009
The authors present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. They 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, they 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, their 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.