15-851 Computation and Deduction
Schedule
- Lectures are Tuesday and Thursday in Wean Hall 5409.
-
The class notes provide additional reading material.
They complement, but do not replace the lecture.
- The schedule is subject to change throughout the semester.
| Date |
Lecture or Recitation |
Reading |
Code |
Homework Due |
|
| Tue | Jan | 16 |
Overview |
mini-ml.pdf, pp. 1-13 |
|
|
| Thu | Jan | 18 |
Natural Semantics |
mini-ml.pdf, pp. 13-24 |
|
|
|
| Tue | Jan | 23 |
Type Preservation |
mini-ml.pdf, pp. 24-31 |
|
|
| Thu | Jan | 25 |
Higher-Order Abstract Syntax |
lf.pdf, pp. 37-50 |
|
2.1, 2.13, 2.14 |
|
| Tue | Jan | 30 |
Judgments as Types |
lf.pdf, pp. 50-63 |
|
|
| Thu | Feb | 1 |
Higher-Level Judgments |
lf.pdf, pp. 63-70 |
|
2.17, 2.7, 2.8 |
|
| Tue | Feb | 6 |
The Elf Programming Language |
elf.pdf,
Twelf User's Guide |
mini-ml, misc |
|
| Thu | Feb | 8 |
Parametric and Hypothetical Judgments |
hypo.pdf |
mini-ml |
|
|
| Tue | Feb | 13 |
A Continuation-Passing Machine |
compile.pdf, pp. 183-193 |
cpm |
|
| Thu | Feb | 15 |
Progress |
compile.pdf, pp. 193-201 |
cpm |
2.12, 4.5, 5.9 |
|
| Tue | Feb | 20 |
Implementing Progress |
compile.pdf, pp. 193-201 |
cpm |
|
| Thu | Feb | 22 |
Bisimulation |
in preparation |
bisim |
|
|
| Tue | Feb | 27 |
Evaluation in Environments |
compile.pdf, pp. 145-153 |
env1 |
|
| Thu | Mar | 1 |
Compiler Correctness |
compile.pdf, pp. 154-170 |
env1, env |
5.11, 3.18 |
|
| Tue | Mar | 6 |
Midterm Examination |
Chapters 1-6 |
|
|
| Thu | Mar | 8 |
Midsemester Holiday (no classes) |
|
|
|
|
| Tue | Mar | 13 |
Parametric Polymorphism |
poly.pdf, pp. 207-212 |
poly |
|
| Thu | Mar | 15 |
Intrinsic Typing |
poly.pdf, pp. 213-221 |
poly |
|
|
| Tue | Mar | 20 |
Constraint-Based Type Inference |
in preparation |
constraints |
|
| Thu | Mar | 22 |
Unification |
in preparation (slides) |
constraints |
5.15 |
|
| Tue | Apr | 3 |
Subtyping |
in preparation |
in preparation |
|
| Thu | Apr | 5 |
Subtyping Constraints |
in preparation |
in preparation |
|
|
| Tue | Apr | 10 |
Intersection Types |
in preparation |
intersect |
|
| Thu | Apr | 12 |
Contextual Semantics |
in preparation |
in preparation |
|
|
| Tue | Apr | 17 |
Parametric Subtyping |
in preparation |
in preparation |
|
| Thu | Apr | 19 |
Refinement Types |
in preparation |
in preparation |
|
|
| Tue | Apr | 24 |
Termination |
in preparation |
in preparation |
|
| Thu | Apr | 26 |
Equational Reasoning |
in preparation |
in preparation |
|
|
| Tue | May | 1 |
Recursive Types |
in preparation |
rectype |
|
| Thu | May | 3 |
Abstract Types |
in preparation (slides) |
abstype |
|
|
[ Home
| Schedule
| Assignments
| Handouts
| Software
| Overview
]
fp@cs
Frank Pfenning
|