| Playlist | schedule page slides as PDF |
Typed Recursion 1 — letrec (3:15)
Type checking recursive functions in Moe. See typed_letrec.rhm.
Typed Recursion 2 — variants (4:58)
Type checking datatypes with variants.
Typed Recursion 3 — interp examples (1:59)
Examples for interp with let_type and match in Moe.
Typed Recursion 4 — interp (3:17)
Implementing interp with let_type and match. See type_case.rhm.
Typed Recursion 5 — typecheck examples (1:53)
Examples for typecheck with let_type and match.
Typed Recursion 6 — typed match (1:23)
Type checking rules for let_type and match.
Typed Recursion 7 — typecheck (4:50)
Implementing typecheck with let_type and match. See type_case.rhm, again.
Typed Recursion 8 — soundness (4:09)
Type soundness and correcting problems with our types rules so far. The repairs described here are included in typed_letrec.rhm and type_case.rhm.