- McClendon Office Hours
- Project 4
- Midterm Scores
- Subtraction
- PolyList
- Natist
- Pairs
- Project 1 Available
- Stacks and Polymorphism
- Project 0 Available

Blog

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.

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 `nat`

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 `nat`

,
subtraction results that would be negative are all `0`

. So it goes.

PolyList.v
is another definition of `list`

that is polymorphic over the type of
the list contents. It is a rewrite of
Natlist.v
with the `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
tasks.

As promised in class, I’ve created a yet another Coq project file
Natlist.v
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
the `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,
Pairs.v, that
includes the modules I presented in class yesterday. Another example
of polymorphism very similar to the
Stacks.v
examples with the additional use of `Notation`

.

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.