Work Plan for Week 5

Material

name file name short version note
Simple Imperative Programs Imp[.html|.v] download

Schedule

date time location type
Monday, 29 September 10:45 - 12:45 CEG - Hall D lecture
Tuesday, 30 September 8:45 - 10:45 CEG - Hall D lecture
Thursday, 2 October 13:45 - 15:45 Pulse - Hall 3 & 6 problem session

Problem Session

file exercises
Imp[.html|.v]
  • define the fixpoint optimize_0plus_b
  • prove that it is sound (optimize_0plus_b_sound) in two ways:
    1. manually, with no Coq automation
    2. using the tacticals to make the proof as short and elegant as possible
  • XtimesYinZ_spec
  • loop_never_stops
  • no_whiles_eqv
If you need help, make a request during the problem session in the Queue or reach out on Mattermost.