Resources

For 505 this quarter we'll be using the following tools and texts to explore PL formalization and program verification:

• Coq : the proof assistant we will be using throughout the course

  • Please use and improve our 505 Community Notes on Coq!

  • The official Coq Tactic Index can be helpful, though it is written as a reference and can be confusing when first learning Coq.

  • Joseph Redmond's Coq Tactic Index has some more guidance on several frequently used tactics.

  • Cornell's 3110 Tactic Index has some nice explanations for key tactics.

  • Appendix A of the FRAP book also has a listing of key tactics, including the friendlier FRAP tactics

• FRAP : the course textbook

  • The FRAP Github repo contains the fully formal version of each chapter's content

  • You should get set up so you can walk through the chapters in CoqIDE

  • VSCoq is also a popular choice of IDE

• The 505 VM : an Ubuntu virtual machine with all the software for the course already set up

  • You can run the VM using Oracle's VirtualBox

  • This article "How To Use OVA Files With VirtualBox" may be helpful

  • Ben and Zach also showed the process in 505 Studio Episode 02

Additional Resources

Though these resources are not required for the course, they can be quite helpful:

• Software Foundations

  • Volume 1 in particular can be helpful if you just getting up to speed with proof assistants.

  • Volume 2 has some more material on PL formalization.

• Xavier Leroy's talk Theorem Provers are a PL Researcher's Best Friend provides some context for the role of proof assistants in modern PL and shows some nice examples.

• Xavier Leroy's blog post Using Coq's evaluation mechanisms in anger goes over some useful details about how to run Gallina programs in Coq.