Lecture

Lectures will be live streamed and archived (requires UW sign-in). This resource is intended for students who are traveling or sick and who have previously discussed their absence from lecture with the instructor. Because this course heavily relies on student participation in lecture, it is essential that everyone attend in person or via the Redmond participatory live stream.

• Lecture 1, April 3 - Introduction, Coq Tutorial, Syntax (FRAP 1, 2) [materials]
  • BasicSyntax.v
  • Polymorphism.v
  • You may want to refer to (and edit!!) our Community Notes on Coq
• Lecture 2, April 10 - Trusting Trust Discussion + Data Abstraction (FRAP 3) [materials]
  • DataAbstraction.v
• Lecture 3, April 17 - Interpreters (FRAP 4) [materials]
  • Interpreters.v
  • FirstClassFunctions.v
• Lecture 4, April 24 - Social Processes Discussion + Transition Systems (FRAP 5) [materials]
  • TransitionSystems.v
  • IntroToProofScripting.v
• Lecture 5, May 1 - Model Checking (FRAP 6) [materials]
  • ModelChecking.v
  • ProofByReflection.v
• Lecture 6, May 8 - Amazon TLA Discussion + Operational Semantics (FRAP 7) [materials]
  • OperationalSemantics.v
  • LogicProgramming.v
• Lecture 7, May 15 - Lambda Calculus and Types (FRAP 10) [materials]
  • LambdaCalculusAndTypeSoundness.v
• Lecture 8, May 22 -BP Discussion + Types and Mutations (FRAP 11) [materials]
  • TypesAndMutation.v
• Lecture 9, May 29 - Hoare Logic (FRAP 12) [materials]
  • HoareLogic.v
• Lecture 10, June 5 - Csmith Discussion + Compiler Verification (FRAP 9) [materials]
  • CompilerCorrectness.v