Embedded Files
505 Studio is a supplement to lecture where Ben and Zach chat about what is going on in 505, step through more code, and goof off. Studio sessions are recorded and posted, and we take topic requests via the course message board.
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!
Episode 01 : March 24 - Coq Intro, Represent Program Syntax (FRAP Chapter 2)
Episode 02 : March 31 - Installing Coq, Some Functional Programming Intro
Episode 03 : April 7 - Dependent Types, Modules and Interfaces in Coq (FRAP Chapter 3)
Episode 04 : April 14 - Tactics, Strengthening Induction Hypotheses
Episode 05 : April 16 - More Transition Systems, Invariant Induction, and Why `exists` has ∀
Episode 06 : April 23 - Model Checking and Comparing Verification Techniques
Episode 07 : May 14 - Lambda Calculus and Church Encodings
Page updated
Report abuse