We make extensive use of Coq theorem prover in this class.

Installing Coq

• You can play around with Coq in a browser using jsCoq, although this is not recommended for serious development.

• Coq platform binaries are available for Mac and Windows. Coq platform includes a stand-alone IDE for Coq development called Coqide.

• Alternatively, you can use Visual Studio Code as an IDE for Coq development with help of a vscode plugin called vscoq. See here for instructions.