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.