Lecture

Lectures will be live streamed and archived (requires sign-in). Because we have a lot of video content this quarter, we've set up a shared doc to collaboratively note timestamps of what topics are discussed when in each video. Please help contribute to the timestamp doc!

This resource is intended for students who are traveling or sick and who have previously discussed their absence from lecture with the course staff, and for review while completing homework assignments. Because this course heavily relies on student participation in lecture, it is essential that everyone attend lecture via Zoom whenever possible!

• Lecture 01 : March 30 - Introduction

• Lecture 02 : April 1 - Coq Tutorial, Abstract Syntax Trees (FRAP Chapter 2)

• Lecture 03 : April 6 - Theorem Provers are a PL Researcher's Best Friend

• Lecture 04 : April 8 - Trusting Trust Discussion, Proofs are Just Functions

• Lecture 05 : April 13 - Interpreters (FRAP Chapter 4)

• Lecture 06 : April 15 - Inductively Defined Predicates, Transition Systems, Invariants (FRAP Chapter 5)

• Lecture 07 : April 20 - Transition Systems, Invariant Induction (FRAP Chapter 5)

• Lecture 08 : April 22 - Social Processes Discusion, Model Checking (FRAP Chapter 6)

• Lecture 09 : April 27 - Operational Semantics (FRAP Chapter 7)

• Lecture 10 : April 29 - Operational Semantics and Inductive Invariants (FRAP Chapter 7)

• Lecture 11 : May 4 - Homework 2 Debrief, Abstract Interpretation Intro, Flow Insensitive Dataflow Analysis (FRAP Chapter 8)

• Lecture 12 : May 6 - Amazon AWS TLA Discussion, Abstraction Interpretation, Flow Sensitive Dataflow Analysis, Formalization in Coq (FRAP Chapter 8)

• Lecture 13 : May 11 - Lambda Calculus and Church Encodings (FRAP Chapter 10)

• Lecture 14 : May 13 - Simply Typed Lambda Calculus (FRAP Chapter 10)

• Lecture 15 : May 18 - Types and Mutation (FRAP Chapter 11)