# Advanced Programming Languages and Verification

## It's all just ~~induction~~ presheaves

## Course Information and Policies

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.

### Staff

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

### Schedule

Lecture MWF 11:30-12:20 Zoom

Section Th 11:30-12:20 Zoom

### Grading

9 homework assignments, each worth 10%

Attendance and participation in lecture and section, worth the remaining 10%

No exams

### Collaboration policy

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.

### Attendance Policy

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.

### Late Policy

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.

### Resources

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)

## Calendar

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