Home
About Coq
Get Coq
Documentation
Community
The Coq Proof Assistant
Keyword: imperative program
HoareTut
: A Tutorial on Reflecting in Coq the generation of Hoare proof obligations
Sylvain Boulmé