CS 3110 Schedule Fall 2008The notes linked below are required reading, but they are not a substitute for attending lecture and recitation. The lectures and recitation sections are tightly coupled: Lectures will assume knowledge from previous sections, and vice-versa. These notes should be read sequentially (Monday's section, Tuesday's lecture, Wednesday's section, Thursday's lecture, etc.). Note: due dates of unreleased assignments are tentative. |
|||
Meeting | Date |
Topic |
|
---|---|---|---|
Introduction to functional programming | |||
Lec. 1 | Aug. 28 | Course overview and background on ML (slides) | |
Rec. 1 | Sep. 1 | Introduction to OCaml syntax (PS1 issued) | |
Lec. 2 | 2 | OCaml syntax and evaluation | |
Rec. 2 | 3 | Tuples, records, and pattern matching | |
Lec. 3 | 4 | Scope, currying and lists | |
4 | OCaml demo, 7–9pm, Upson B7 | ||
Rec. 3 | 8 | Printing, side effects, and exceptions | |
Lec. 4 | 9 | Variants, recursive types, and polymorphism (PS1 due, PS2 issued) | |
Rec. 4 | 10 | Pattern-matching pitfalls, more parameterized types | |
Lec. 5 | 11 | Substitution model of evaluation | |
Rec. 5 | 15 | Folding and tail recursion | |
Modular programming and function specifications | |||
Lec. 6 | 16 | Specifications | |
Rec. 6 | 17 | Functional examples, structures and signatures | |
Lec. 7 | 18 | Modules and data abstractions (PS2 due) (PS3 issued) | |
Rec. 7 | 22 | Functional stacks and queues | |
Lec. 8 | 23 | Abstraction functions | |
Rec. 8 | 24 | Dictionaries and association lists | |
Lec. 9 | 25 | Representation and module invariants | |
Rec. 9 | 29 | Set and map interfaces and functors | |
Reasoning about correctness | |||
Lec. 10 | 30 | Module dependency diagrams, testing (slides) | |
Rec. 10 | Oct. 1 | Testing and code review | |
Lec. 11 | 2 | Verification | |
Rec. 11 | 6 | More inductive correctness proofs (PS3 due, PS4 issued) | |
Lec. 12 | 7 | Verifying data abstractions, propositional logic | |
Rec. 12 | 8 | Propositional logic and proofs (PDF) | |
Lec. 13 | 9 | Predicate logic, Hoare logic for formal verification | |
Fall break: Oct. 11–14 | |||
Rec. 13 | 15 | Using propositional and predicate logic | |
Lec. 14 | 16 | Prelim review | |
October 16 | Preliminary Exam, 7:30–9:00pm, McGraw 165 (Closed-book. Covers material through Recitation 12 and PS3.) | ||
Rec. 14 | 20 | Prelim wrap-up, review of Hoare logic | |
Lec. 15 | 21 | Formal verification with functions and data abstraction | |
Rec. 15 | 22 | Mutable data structures: refs and arrays | |
Lec. 16 | 23 | Formal verification demo, mutable data abstractions | |
Reasoning about performance | |||
Rec. 16 | 27 | Asymptotic complexity and binary search trees | |
Lec. 17 | 28 | Implementing mutable data abstractions (PS4 due, PS5 issued) | |
Rec. 17 | 29 | PS5 overview | |
Lec. 18 | 30 | Asymptotic complexity and recurrences | |
Rec. 18 | Nov. 3 | Solving recurrences with induction | |
Lec. 19 | 4 | Substitution and master methods | |
Rec. 19 | 5 | Using the substitution and master methods | |
Data structures and algorithms | |||
Lec. 20 | 6 | Red-black trees | |
Rec. 20 | 10 | Concurrency and message passing | |
Lec. 21 | 11 | Hash tables and hash functions | |
Rec. 21 | 12 | Representing and traversing graphs, Garbage collection | |
Lec. 22 | 13 | Resizing hash tables and amortized analysis (PS5 due, PS6 issued) | |
Rec. 22 | 17 | PS6 overview | |
Lec. 23 | 18 | Memoization | |
Rec. 23 | 19 | Amortized analysis examples | |
Below the OCaml abstraction | |||
Lec. 24 | 20 | Locality | |
Rec. 24 | 24 | B-trees | |
Lec. 25 | 25 | Splay trees | |
Thanksgiving recess: Nov. 26–30 | |||
Programming paradigms | |||
Rec. 25 | Dec. 1 | Streams and other laziness | |
Lec. 26 | 2 | Functional programming in mainstream languages | |
Rec. 26 | 3 | Lambda calculus | |
Lec. 27 | 4 | Logic programming and reversible computation (JMatch website) | |
Dec. 9 | The 312 Tournament, Upson B17, 7:30–9:30pm (pizza provided) | ||
Dec. 18 | Final Exam, 2–4:30pm,
Olin 155 |