As many of you know, Brian McClendon has joined our faculty as a research professor. As developer of Google Earth and VP at both Google and Uber, Brian has great insight into both the technical and business side of computer science. Prof. McClendon is going to have general office hours if you want to come in and talk about a project or a career path. The first will be this Thursday 1pm-4:30pm. Sign up here.
Unfortunately, there are going to be lots of schedule changes at the end of the semester due to my trael. Important dates and changes are as follows:
If you miss everything else, do not miss the exam on 12/7!
Project 4 is now available on Blackboard.
Assuming that I was able to successfully use blackboard, your miterm exam scores are available on the class blackboard site. The exam was great. I am quite happy with the class performance.
Someone in class today asked about closure of subtraction over
in Coq. Actually, that wasn’t the question but it’s close enough for
jazz. I commented that
0 - 1 = 0 in Coq to a number of well-deserved
snickers. Turns out it’s true. To make subtraction closed over
subtraction results that would be negative are all
0. So it goes.
is another definition of
list that is polymorphic over the type of
the list contents. It is a rewrite of
list type parameterized over content type. All proofs and
definitions are re-done.
For your reading enjoyment I’ve also added some basic LTac definitions
that take advantage of Coq’s proof scripting capability.
LTac is a
powerful language for writing tactics and reusing proofs. IN this
example I use it to automate induction proofs. I also use
autorewrite and rewrite databases to automate some mundane rewriting
As promised in class, I’ve created a yet another Coq project file
that includes the
natlist examples I did in class. Almost everything
in the file is from Software Foundations, but I added a couple of
things that Pierce does not talk about. One is the use of lemmas and
assert command and the other is a peek at using Ltac to simplify
proofs. We will go over the rest of the module in class, but will
likely not do much with Ltac right now. Just wanted to give you a
taste of where we’re headed.
I’ve created a yet another Coq project file,
includes the modules I presented in class yesterday. Another example
of polymorphism very similar to the
examples with the additional use of
Project 1 is now availabe in the projects section. It is a moderately more difficult problem set, but should still be reasonably easy. Some proofs require commands we have not learned as of September 14, but I wanted to let you get started now and experiment on your own.
I’ve created a Coq project file, Stacks.v, that includes the various stacks we’ve defined in class to illustrate poloymorphism in Coq. You will find several modules in the file each with a definition and several examples. There’s documentation in the file and I’ll add more when I have a chance. For now, load the file in Coq and play around.
There are no proofs at the moment, but you’ll discover the reason for that when you see your next project assignment…
Project 0 is now availabe in the projects section. It is a warm-up project intended to get you used to using the verifier. All proofs and definitions can be completed using techniques learned in class.