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.
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.
Small changes and additional information about the midterm that I will go over in class today.
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.
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.
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:
There are many more tactics and we’ve not learned much about automation, but this is a good start.
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.
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 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.