Community Docs
Below we link to a variety of notes and reference documents you may find helpful throughout 505. Contributing to the community notes and reference docs provides great opportunity to practice writing, collaborate with colleagues, and help build a supportive community! Please make sure to note your contributions in the 505 Gradesope.
Community Notes
We’ll be collaboratively developing 505 Community Notes throughout the quarter.
Also check out the notes from the previous offering of the course.
A great way to contribute to the community is porting and cleaning these up into our own version!
Please help out by drafting, editing, or discussing any of the following:
Summaries and tutorials of concepts from lecture
Examples and figures that highlight important PL concepts
Overviews and walkthroughs of key proofs in Coq or traditional, “pen and paper” style
See the Community Docs section of the 505 Overview for additional contribution suggestions, challenge point details, and more.
Reference Docs
Instructions for installing Coq, VS Code, and plugins on various platforms
Guidance and best practices for writing proofs in Coq and traditional "pen and paper" style
This document shows more of what’s going on “under the hood” at a lower level when we use Coq.
Warning: The Coq Fundamentals doc is written in a different style than lecture or homework!
Additional Resources, Interesting Links
Coq Tactic Indices and Search Commands
Textbooks, Notes, and Courses
Advanced Programming Languages and Verification (UW CSE 490P) by James Wilcox
This course is similar to 505, but with less emphasis on mechanized proof.
We'll borrowing lots of infrastructure, examples, and explanations from 490P; check out its videos (UW CSE NetID required)!
Formal Reasoning About Programs (FRAP) by Adam Chlipala
505 is heavily influenced by FRAP, borrowing much of its narrative as well as several examples.
Certified Programming with Dependent Types (CPDT) is also excellent, though more advanced.
The Software Foundations series provides several great Coq-based Computer Science textbooks.
Volume 1: Logical Foundations provides many examples and a smooth introduction to Coq.
Volume 2: Programming Language Foundations focuses more on verification and formalizing PLs.
Introduction to the Calculus of Inductive Constructions by Christine Paulin-Mohring
Provides a concise, technical overview of using dependent type theory for theorem proving.
Miscellaneous
Theorem Provers are a PL Researcher's Best Friend - Xavier Leroy - 2020
In this talk, Leroy (of OCaml and CompCert fame) motivates the use of proof assistants in PL research and shows its influence in compiler verification.
Leroy has also developed a self-contained, short course on formally verifying a small compiler which 505 participants may want to explore after the quarter.
The Computerphile channel has some high-level introductions to a couple of the ideas we'll detail in 505.
