| Playlist | schedule page slides as PDF |
Type 1 — motivation (8:52)
Expressions vs. “well-formed” expressions. You could skip this video, but it’s trying to get at what a type system is really about.
Type 2 — types (3:05)
Types as an approach to well-formedness.
Type 3 — type rules (3:17)
Type rules in the traditional, math-ish notation.
Type 4 — conditionals (2:58)
Type rules for conditionals.
Type 5 — functions (5:51)
Type rules for functions.
Type 6 — function calls (2:45)
Type rules for function calls.
Type 7 — multi-argument function calls (1:48)
An aside on type rules for multi-argument functions and funicton calls, as set-up for the homework assignment.
Type 8 — typecheck (6:03)
Implementing typecheck. See typed-lambda.rkt.
Type 9 — typecheck vs. interp (1:06)
A reminder that typecheck and interp do not call each other.
Type 10 — pairs (2:42)
Type rules for pairs, as set-up for the homework assignment.