- Final Exam
- Imp and IndProp
- Homework Scores
- Homework Grading
- Final Homework Excercises
- Midterm Clarification
- Midterm Exam
- Midterm Exam Info
- Classes Fall 24
- Tactics So Far

Blog

Excercises I will grade from `Imp.v`

and `IndProp.v`

are listed
below. You can do more if you want and I will grade them, but this is
what I will definitely incldue:

Most of these are 1 star with a few more difficult proofs at the end. No 4 or 5 star proofs. I’m not asking you to prove The Pumping Lemma even though Pierce would.

`close_refl_trans`

`perm`

`ev_double`

`inversion_pactice`

`ev5_nonsense`

`ev_sum`

`ev'_ev`

`ev_ev__ev`

`ev_plus_plus`

`total_relation`

`empty_relation`

`subsequence`

`reflect`

The `Imp.v`

chapter doesn’t have too many truly 1 star problems. Set
aside some time to work on these, but none of them are horrible.

`optimize_0plus_b_sound`

`optimize`

(4 star, so be careful)`bevalR`

`ceval_example2`

`loop_never_stops`

`no_whiles_eqv`

`stack_compiler`

(particularly cool)