| 1 |
2/24 |
Functional Programming |
1 |
1.1—1.5 |
Functional Programming (1) |
|
|
|
2/26 |
|
|
1.6—1.9 |
Functional Programming (2) |
HW1 |
|
| 2 |
3/3 |
|
|
1.10—1.11 |
Functional Programming (3) |
|
|
|
3/5 |
Inductive Definitions |
2 |
2.1—2.3 |
Inductive Definitions |
HW2 |
HW1 |
| 3 |
3/10 |
|
|
2.4—2.5 |
Inductive Proofs |
|
|
|
3/12 |
Untyped λ-Calculus |
3 |
3.1—3.2 |
λ-Calculus (Syntax, Semantics) |
HW3 |
HW2 |
| 4 |
3/17 |
|
|
3.3 |
λ-Calculus (Substitution) |
|
|
|
3/19 |
|
|
3.4—3.5 |
λ-Calculus (Programming) |
HW4 |
HW3 |
| 5 |
3/24 |
Simply Typed λ-Calculus |
4, 5 |
4.1—4.3 |
Simply Typed λ-Calculus |
|
|
|
3/26 |
|
|
5.1—5.4 |
Extensions |
|
|
| 6 |
3/31 |
|
|
4.4, 5.6 |
Type Safety |
HW5 |
HW4 |
|
4/2 |
|
|
3.7 |
De Bruijn Indexes |
|
|
| 7 |
4/7 |
- More Operational Semantics |
8, 9 |
8.1—8.2 |
Evaluation Contexts |
|
|
|
4/9 |
|
|
8.3—9.1 |
Abstract Machine C, Environments |
HW6 |
HW5 (4/12) |
| 8 |
4/14 |
|
|
|
Midterm Exam (9:15am—10:45am) |
|
|
|
4/16 |
|
|
|
No Class |
|
|
| 9 |
4/21 |
|
|
9.2—9.4 |
Closures, Abstract Machine E |
|
|
|
4/23 |
- More Language Features |
6, 10, 12 |
12.1—12.3 |
Recursive Types |
|
|
| 10 |
4/28 |
|
|
10.1—10.4 |
Exceptions, Continuations |
HW7 |
HW6 |
|
4/30 |
|
|
6.1—6.3 |
Mutable References |
|
|
| 11 |
5/5 |
|
|
|
No Class (Children’s Day) |
|
|
|
5/7 |
|
|
|
No Class (POSTECH Festival) |
|
|
| 12 |
5/12 |
Object Calculus |
11 |
11.1—11.3 |
Subtyping |
|
|
|
5/14 |
|
|
Link |
Featherweight Java |
|
|
| 13 |
5/19 |
Polymorphic λ-Calculus |
13 |
13.1—13.3 |
System F |
HW8 |
HW7 |
|
5/21 |
|
|
13.4—13.5 |
Let-polymorphism |
|
|
| 14 |
5/26 |
Theorem Proving |
- |
Link, Link |
Curry-Howard Correspondence |
|
|
|
5/28 |
|
|
Link, Link |
Dependent Types |
HW9 |
HW8 (5/31) |
| 15 |
6/2 |
|
|
Link, Link |
Theorem Proving in Lean (1, 2 / 3, 4, 5) |
|
|
|
6/4 |
Conclusion |
- |
- |
Course Wrap-Up |
|
|
| 16 |
6/9 |
|
|
|
Final Exam (9:15am—10:45am) |
|
|
|
6/11 |
|
|
|
No Class |
|
HW9 |