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

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

• 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
•