Work Plan for Week 6

Material

name	file name	short version	note
Hoare Logic, Part I	Hoare[.html|.v]	download	read the whole chapter, in particular, step through the Rocq proofs of the Hoare logic proof rules
Hoare Logic, Part II	Hoare2[.html|.v]		read the whole chapter, in particular the part on implementation in Rocq

Schedule

date	time	location	type
Monday, 6 October	10:45 - 12:45	CEG - Hall D	lecture
Tuesday, 7 October	8:45 - 10:45	CEG - Hall D	lecture
Thursday, 9 October	13:45 - 15:45	Echo - Hall B	problem session

Problem Session

file	exercises
Hoare[.html|.v]	read through the following subsections in “Proof Rules”: “Skip”, “Sequencing”, “Assignment” hoare_asgn_examples1 hoare_asgn_examples2 hoare_asgn_wrong hoare_asgn_fwd hoare_asgn_fwd_exists
Hoare2[.html|.v]	if_minus_plus_reloaded if_minus_plus_correct div_mod_outer_triple_valid slow_assignment parity sqrt

---

If you need help, make a request during the problem session in the Queue or reach out on Mattermost.