EECS 755 Blog

Final Exam

The final is here. LaTeX source is here should you want to use it. Submit your solution via Canvas by 2:30 May 9.

Imp and IndProp

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:

IndProp.v

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

Imp.v

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)

Homework Scores

I just took all grades that I’ve posted offline until I can repost corrected scores. Should be later today. My auto-grader was producing bad values and freaking people out. That is definitely not what I intended and I’m sorry if I caused undo stress. I believe the problem is corrected and I’ve regenerated grades. Still need to check them and post scores.

One issue exists that I need your help with. When I post grades you may see no grade for an assignment you submitted. This is almost certainly because your proof file crashed. Likely due to a missing Admitted statement or due to inclusion of an Abort command. Missing Admitted causes a proof to hang while Abort terminates the proof process. Either of these causes the test file to fail. What I need you to do is fix the error and resubmit. Your test file needs to generate output and terminate without throwing errors. I believe you can do this via Canvas or even better just send me email.

I will ping you again when grades are posted. If you already know your assignment files throw errors, you can go ahead and start fixing that.

Homework Grading

Homework grades are gradualing making it to the Canvas site. Unfortunately, my auto-grader has not been formally verified and is not perfect. Please don’t freak out if you see a score that you don’t expect. I plan on looking at every grade that is unusual before I make grades final. If you want to contact me (email or otherwise) about homework scores, please feel free.

Final Homework Excercises

As promised in class, here is a list of problems you should choose from for your last 2 homework assignments. I will grade the same way I have been, just limited to these assignments. If you want to do others, I will happily grade them and give you extra homework points.

Unfortunately exercises are not numbered, so I will simply list the theorems to prove by name.

Equiv.v

1. skip_right
2. if_false
3. swap_if_branches
4. while_true
5. seq_assoc
6. assign_aequiv
7. CIf_congruence

We did not go over assignment in any detail, but I think the last couple of proofs are quite doable.

Hoare.v

1. hoare_post_true
2. hoare_pre_false
3. hoare_asgn_examples1
4. hoare_asgn_examples2
5. hoare_asgn_wrong
6. hoare_asgn_forward
7. hoare_asgn_fwd_exists
8. assertion_sub_ex1'
9. assertion_sub_ex2'
10. if_minus_plus

All homeworks are due on the last day of finals, regardless of what Canvas says. I will try to remember to update the dates.

Midterm Clarification

On Exercise 2 don’t worry about the “guessing decreasing argument” issue the Coq type checker brings up. When I wrote the exam I did not anticipate anyone trying to actually code the tree structure up in the prover because it was intended to be done in class. Assume that Coq can find the decreasing argument. There is a solution to this, but it’s not what I want you spending your time on.

Midterm Exam

The midterm is here. LaTeX source is here should you want to use it. Submit your solution by email or Canvas by 2:30 Friday.

Midterm Exam Info

Small changes and additional information about the midterm that I will go over in class today.

1. Midterm will be on Thursday, March 28. I recently learned I will be traveling to Washington, DC that day. Thus the change
2. The exam will be available online. I will release it at 2:30pm on the 28th and you will submit it at 5:00pm the same day.
3. The exam will be open book, open notes and will cover everything up to IndProp. I will provide a topic list next class period.

Sorry for the late change, but I hope having 2.5 hours and open book will make up for it.

Classes Fall 24

Many of you have asked what will be offered in Fall 2024 related to programming languages and specifically what I might be teaching. After checking the KU classes website I discovered that I was not scheduled for any courses. This was not intended. I will be offering EECS 762 in the fall which is our course on operational semantics. Tell your friends as I’m guessing no one knows the course is being taught.

Tactics So Far

We’ve reached a point where we’ve got enough tactics to do some real work. Here are tactics that we’ve seen in class as of 2024-20-20:

• intros: move hypotheses/variables from goal to context
• reflexivity: finish the proof (when the goal looks like e = e)
• apply: prove goal using a hypothesis, lemma, or constructor
• apply… in H: apply a hypothesis, lemma, or constructor to a hypothesis in the context (forward reasoning)
• apply… with…: explicitly specify values for variables that cannot be determined by pattern matching
• simpl: simplify computations in the goal
• simpl in H: … or a hypothesis
• rewrite: use an equality hypothesis (or lemma) to rewrite the goal
• rewrite … in H: … or a hypothesis
• symmetry: changes a goal of the form t=u into u=t
• symmetry in H: changes a hypothesis of the form t=u into u=t
• transitivity y: prove a goal x=z by proving two new subgoals, x=y and y=z
• unfold: replace a defined constant by its right-hand side in the goal
• unfold… in H: … or a hypothesis
• destruct… as…: case analysis on values of inductively defined types
• destruct… eqn:…: specify the name of an equation to be added to the context, recording the result of the case analysis
• induction… as…: induction on values of inductively defined types
• injection… as…: reason by injectivity on equalities between values of inductively defined types
• discriminate: reason by disjointness of constructors on equalities between values of inductively defined types
• assert (H: e) (or assert (e) as H): introduce a “local lemma” e and call it H

There are many more tactics and we’ve not learned much about automation, but this is a good start.

Homework Grading

I have updated the grading policy for homework to match what we discussed in class on February 5. If you object to these changes, I will grade your work as defined in the original syllabus. However, the updates are designed to make homework less stressful. Hopefully everyone will approve.

Basics Updated

I just pushed new versions of Basics.v and BasicsTest.v to the website. They should be downloadable now. Feel free to take an extra day or two to complete the additional exercises.

Welcome

Welcome to the EECS 755 blog for Spring 2024. You will find late-breaking information about the class and associated projects and exams here. The blog is available via RSS feed if you use an RSS aggregator.

Please keep in mind that this is a math class. We will treat programs as mathematical objects and we will be doing proofs from day one. Our proofs are done in an automated checker built into an IDE, but they are still proofs. We will move quickly and I expect you to install new software, correct syntax problems, and debug code on your own. I will teach you new material you need to know, but we don’t have time for extensive review of prerequisite material.

As you’re getting started it would be a good idea to install Coq on your system of choice. It is strongly suggested that you start with CoqIDE or VSCode. CoqIDE provides a drag-and-drop installation as well as an IDE for Coq. It is the simplest way to get started. VSCode with VSCoq is a far more powerful development environment that requires a bit more heavy lifting to install. Definitely worth the effort. If you are an emacs and linux user then ProofGeneral is a great option. I suspect far more of you use VSCode these days than emacs.

For reference, I am an emacs/ProofGeneral user while most of my students are VSCode users. While this prompts many spirited discussions in the lab, both work quite well.