This archive contains a Coq formalization of parts of the completeness proof of the paper "Completeness and complexity of reasoning about call-by-value in Hoare logic".