- Using Coq
- The Coq system is installed in a unix environment and available to you from the graduate laboratory in STE 2051. You should run the system on a solaris machine. See the information on Logging on to SITE's Unix Servers. To run Coq, you need to follow the instructions on the SITE Software page. Version 8.0 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. It runs on several operating systems including linux, Solaris, and Windows.
- 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 a SITE student, you must be registered in the course to get an account. If not, see me first.)
- You can also log in remotely and get access to a solaris machine. Use ssh to access ugate.site.uottawa.ca.
- Propositional Logic in Coq
- Example Coq session corresponding to lectures on 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
- Example Coq session corresponding to lectures on 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.