Resources

In addition to Formal Reasoning About Programs (FRAP), the primary textbook for 505, you may find some of these additional resources helpful:

• Software Foundations (SF)
• Types and Programming Languages (TAPL)
• Certified Programming with Dependent Types (CPDT)
• The Little Typer
• Previous offerings of CSE 505

We also set up an Ubuntu virtual machine with Coq and FRAP installed: csep505-19sp VM (~ 6 GB)

• VitualBox
• How to use OVA images with VirtualBox

A lot of times when you're stuck in a proof, you just need to find the right tactic. These references might help:

• Community Notes on Coq — written by you!
  • Here are instructions to access the document via your CSE netid (which is, confusingly, separate from your UW netid, even though you probably have the same username for both).
    • In the top right corner of the google docs page, click on your little account icon, then click add account.
    • Enter your netid @cs.washington.edu, then press next, then it should take you to a CSE looking sign in page.
    • Log in there.
    • You are now signed into multiple accounts on Google docs. You may need to select the correct account by dropping down your little account icon in order to view the document.
  • Please get in touch via Mattermost or email if you have trouble.
• Joe's Tactic Index
• FRAP Tactic Index in Appendix A
• Cornell 3110 Tactic Index
• Coq Tactic Index

Some interesting links folks in 505 may want to explore:

• A Vindication of Program Verification
• Social processes, program verification and all that
• Pokémon Yellow Total Control Hack
• Van Eck Phreaking
• Left pad debacle: The Register, Business Insider
• Bloomberg on Compromised Hardware Oct, 2018
• Greg Nelson's Thesis (Sections 1.1 and 1.2)
• Euler Conjecture Counterexample