Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs

Zenodo (CERN European Organization for Nuclear Research) 2026 Open access

Read full text
Authors: Shushu Wu, C.G. Yang, Xiwei Wu, Qinxiang Cao
DOI: 10.5281/zenodo.20540814
Cited by: 1

Abstract

Machine-checked Rocq (formerly Coq) formalization accompanying the ICFP 2026 functional pearl **Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs.** The development demonstrates a modular two-layer verification approach in which algorithm-level invariants are transferred to implementation-level proofs by expressing implementation correctness as a **relational Hoare quadruple** and annotating the abstract algorithm with `assert` statements.

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
4 June 2026