- Using Coq
- The Coq system, Windows version, is available for you to use in the SITE 0110 Computer Lab. You can run either Coq (which opens a Command Prompt Window) or CoqIDE (preferred). The class demo uses CoqIDE. Version 8.3pl2 is available on these machines.
- The Coq system is also installed in a unix environment and available to you from the graduate laboratory in STE 2051 or by remote access. See the information on Logging on to SITE's Unix Servers. Version 8.2pl1 is the version that is available on these machines.
- You can get the Coq system here if you want to install it on your own computer.
- If you do not have an account which gives you access to the machines in the SITE graduate lab (STE 2051), you can get one. Click here for instructions. (If you are not an EECS student, you must be registered in the course to get an account. If not, see me first.)
- Propositional Logic in Coq
- Examples1.v: Type "Load Examples1." to Coq to make these examples and derived rules available. (This file contains all the propositional examples covered during lectures, in a form that can be loaded directly into Coq.)
- Predicate Logic in Coq
- Examples2.v: This file contains the predicate logic examples covered in class. They are in a form that can be loaded directly into Coq.
- protocol.v: This file contains part of the proof of the property of the SQR protocol covered in class. The rest of the proof is left as an exercise.
- Notes on Coq commands that correspond to natural deduction inference rules.
- The Coq tutorial is available in html, or pdf. Material to be covered in class includes Chapter 1, Sections 1.1, 1.2, and 1.3 on propositional logic, and Chapter 1, Section 1.4 on predicate logic.
- Further Coq documentation is also available online.
- Coq's main web page is here.
