This is an advanced undergraduate special topics course on programming languages and verification. We'll aim to balance theory and practice, with lecture leaning a little bit theoretical and assignments leaning a little bit practical. We expect the course to be challenging and fast-paced. In particular, the weekly homework assignments are about a full week's worth of work assuming you take a normal course load in addition to this course.
This is a difficult time. The course will be taught entirely online via Zoom. We will record lectures and section for archival purposes, but real-time attendance is mandatory except in extenuating circumstances. Please get in touch to discuss any accommodations you may need to succeed in this course.
James Wilcox (jrw12@cs.washington.edu)
Office hours (via Zoom): Tuesdays 1:30-2:30 and by appointment
Brendan Murphy (bsmurphy@uw.edu)
Office hours (via Zoom): Thursdays 3:30-4:30 and by appointment
Lecture MWF 11:30-12:20 Zoom
Section Th 11:30-12:20 Zoom
9 homework assignments, each worth 10%
Attendance and participation in lecture and section, worth the remaining 10%
No exams
You are encouraged to discuss the homework assignments with your classmates and to collaborate. However, the work you submit should be your own. Do not look at anyone else's work or solution. Do not show your work or solution to anyone else. If you work closely with another student, please include a note to that effect in your submission.
Real-time attendance at lecture and section is mandatory except in extenuating circumstances. If you must miss any of these, please notify all staff by email as soon as possible.
All assignments are due on a Wednesday at 5:59:59pm Pacific time. You have 10 late days to use throughout the quarter. Late days are indivisible, and each late day extends the deadline by 24 hours. In other words, if you submit at 6:00:00pm Pacific time on a Wednesday, you are charged 1 whole late day and have until 5:59:59pm on Thursday to keep submitting without spending additional late days.
Discussion on CSE Mattermost (invite link to create account)
OCaml
OCaml reference manual (language, compiler, and standard library)
Source code for the OCaml standard library (when the docs aren't enough...)
Menhir (parser generator)
Dune documentation (build system)
Real World OCaml (online textbook about OCaml)
Fuzzing with afl (3rd-party repository with some nice OCaml-afl examples)
Z3
SMT2 Lib standard (See Figure 3.6 on page 45 for a list of standardized commands accepted by compliant solvers.)
Books
Optional text: Types and Programming Languages by Benjamin Pierce
Optional text: Practical Foundations for Programming Languages by Bob Harper
Course materials
All publicly accessible lecture materials (slides, demo code, etc.)
All video recordings (CSE login or special permission required)
Everything in the future is subject to change. Everything in the past is subject to inaccuracy.
Week 1: Welcome to Programming Languages! It's all just induction
(M 3/30) Lecture 1: Introductions, Zoom usage and etiquette, syllabus, syntax & semantics, induction, interpreters
(W) Lecture 2: Operational semantics, long horizontal lines, runtime errors, more induction
(W) Homework 1 out: Programming part (Gitlab folder); Theory part (TeX source); Implementing interpreters and type checkers; practice with induction and type safety proofs
(Th) Section 1: OCaml, parsing with Menhir, ASTs, interpreters, type checkers, course grading infrastructure
(F) Lecture 3: Type systems, type checkers, type safety, induction, variables
Week 2: Welcome to Verification! It's all just induction
(M 4/6) Lecture 4: Verification, contrasted with PL, informal intro to IMP, transition systems, inductive invariants
(W) Lecture 5: Z3 for transition systems, logic, satisfiability and validity, syntax and semantics of IMP
(W) Homework 1 (Programming) due
(W) Homework 2 out: Programming part (Gitlab folder); Theory part (TeX source); Implementing tools on top of Z3, interpreter and typechecker for IMP, practice with transition systems
(Th) Section 2: Intro to using Z3 as a human and programmatically
(Th) Homework 1 (Theory) due
(F) Lecture 6: More semantics of IMP, "direct" verification of IMP programs, type system for IMP, type safety for IMP
Week 3: All about functions
(M 4/13) Lecture 7: Canceled for James's health and happiness
(W) Lecture 7+8: Simply typed lambda calculus, substitution (defined by induction), variable binding, type safety of STLC (by induction), adding features to STLC
(W) Homework 2 (Programming part) due
(W) Homework 3 out: Programming part (Gitlab folder); Theory part (TeX source); Implementing lambda calculi, practice adding features to STLC both in theory and practice
Note that the theory part will be updated in place after each lecture to include problems from that day. Check back on Friday for the full set.
(Th) Section 3: Untyped lambda calculus, examples of expressive power
(F) Lecture 9: Limits of expressiveness in STLC, termination of STLC, coolest induction ever
Week 4: Hoare Logic
(M 4/20) Lecture 10: Intro to Hoare logic, rules of Hoare logic, inductive invariants
(M) Homework 2 (Theory part): one problem of your choice due
(W) Lecture 11: Soundness of Hoare logic (by induction)
(W) Homework 4 out: Programming part on Gitlab; Theory part (TeX source); Implementing Hoare logic, practice with Dafny, adding stuff to Hoare logic
(Th) Section 4: Fun with Dafny!
(F) Lecture 12: Verification condition generation; weakest preconditions
Week 5: Parametric polymorphism
(M 4/27) Lecture 13: System F and parametric polymorphism, examples of expressive power, type safety
(M) Homework 3 due
(W) Lecture 14: More System F, typed Church encodings in general, type inference, unification, why type inference is a bad idea š¶
(W) Homework 5 out: Programming part on Gitlab; Theory part (TeX source); Implementing polymorphism and type inference, practice with free theorems
(Th) Section 5: Free Theorems and Parametricity, informally
(F) Lecture 15: Termination of System F, the even coolest-er induction ever, proving free theorems, BONUS: binary logical relations and proving relational parametricity
Week 6: Inferring inductive invariants for transition systems
(M 5/4) Lecture 16: A PL person's perspective on propositional and first-order logic, transition systems in logic
(W) Lecture 17: Infinite state systems in first-order logic, the Lock Serviceā¢
(Th) Section 6: Capture avoiding substitution
(F) Lecture 18: Model theory of FOL; Effectively Propositional Reasoning (EPR); the small model property and decidability
Week 7: Adding stuff to typed lambda calculus
(M 5/11) Lecture 19: Sum types; local reduction and expansion; introduction and elimination forms
(W) Lecture 20: Canceled
(W) Homework 7 out: OPTIONAL theory part (TeX source); Inductive types
(Th) Section 7: Canceled
(F) Lecture 21: Inductively defined data types; the generic form of an eliminator
Week 8: Inductive types, intro to dependent types
(M 5/18) Lecture 22: Alpha equivalence and capture-avoiding substitution done right; more inductive types
(W) Lecture 23: Semantics of inductive types; nested inductive types
(Th) Section 8: GADTs
(F) Lecture 24: Intro to dependent types
Week 9: Dependent types except mostly just no class
(M 5/25) Memorial Day - no class
(W) Lecture 25: Dependent eliminators; inductive data in dependent type theory
(Th) Section 9: Practice with dependent types
(F) Lecture: Canceled
Week 10: More dependent types, course wrap up, grad school pitch, industry pitch
(M 6/1) Lecture 26: Propositions as types, inductively defined propositions, propositional equality
(W) Lecture 27: More propositional equality
(Th) Section 10: Cancelled
(F) Lecture 28: Course summary and takeaways; What it's like to go to grad school in PL and verification; What it's like to work in industry in PL and verification