Section is held on Fridays, 3pm-4pm in MD 223 (except Friday Feb 14, when it is in MD 323). Section attendance is not required. Sections are recorded but not live-streamed.
The following is a list of the sections that were held, and the topic/problems covered.
Videos of the lecture and section are available here. (Make sure to log in, and look on the left of the page for "Lecture Videos", etc.) The same site also provides live streams for lecture.
| Date | Topic |
|---|---|
| Fri 14-Feb | Inductive proofs. |
| Fri 21-Feb | Denotational semantics and fix points. |
| Fri 28-Feb | Continuation-passing style translation. |
| Fri 7-Mar | Typing derivations. |
| Fri 14-Mar | Type inference. |
| Fri 28-Mar | Subtyping and the Curry-Howard Isomporphism in Coq. Nats.v, SortTest.v, stlc.v |
| Fri 4-Apr | Contracts and blame. |
| Wed 9-Apr | Introduction to Programming in Haskell. Haskell file |
| Fri 11-Apr | Hoare logic. |
| Fri 18-Apr | 0CFA example (continued from lecture), abstract interpretation of while loops. |
| Fri 25-Apr | Datalog. |
| Fri 2-May | Existential types. |