EECS 755

Software Requirements Modeling and Analysis


Stacks and Polymorphism

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…