Typed Recursion Videos for CS 5510/6510

• Typed Recursion 1 — letrec (3:45)

  Type checking recursive functions. See typed-letrec.rkt.

• Typed Recursion 2 — variants (5:25)

  Type checking datatypes with variants.

  The video and slides for this part use pair, fst, and snd for “raw” pairs, while previous slides use cons, first, and rest. The earlier slides/videos really should be changed to be consistent with this video, so that cons, first, and rest are used only for lists, as opposed to raw pairs.

• Typed Recursion 3 — interp examples (3:12)

  Examples for interp with let-type and type-case.

• Typed Recursion 4 — interp (3:21)

  Implementing interp with let-type and type-case. See type-case.rkt.

• Typed Recursion 5 — typecheck examples (2:36)

  Examples for typecheck with let-type and type-case.

• Typed Recursion 6 — typecheck (8:04)

  Implementing typecheck with let-type and type-case. See type-case.rkt, again.

• Typed Recursion 7 — soundness (4:57)

  Type soundness and problems with our types rules so far. The repairs described here are included in typed-letrec.rkt and type-case.rkt.