Course Info

Time and place:

MWF 10:30-11:20 in 500 AKW

Instructor:

Valery Trifonov
Office: 304 AKW, 203-432-7606
Office hours: MF 2:30-3:30, W 2:30-3:00 or by appt

TA:

Zhanyong Wan

Course newsgroup:

yale.cs.cs430

Texts

The textbook is

John C. Reynolds, Theories of Programming Languages, Cambridge University Press, 1998, ISBN 0-521-59414-6.

Additional texts available online (links to local copies):

Robert Harper's draft notes on Type Systems for Programming Languages (ps.gz, ps)

Benjamin C. Pierce's draft notes on Type Systems (ps.gz, ps)

Grading Policy

Homework assignments will contribute 80% of the course grade, the other 20% will come from the score on the final exam. The final exam will be take-home; the problems will be posted on the assignments page at 9am on May 2, and the results will be due by 9am on May 4.

Unless otherwise noted, homework is due by midnight of the due date. It may be e-mailed to the TA or the instructor, or a hard copy may be submitted in person to the instructor or dropped in either mailbox (313 or 304 in AKW).

Late submission policy: Each student has a total of 6 late days to use at their discretion with no penalty. Otherwise, the penalty is 10% of the grade per late day. No homework late for more than 10 days (including discretionary late days) will be accepted without permission from the Dean. Please let the TA know if you are using your discretionary late days when submitting homework after the due date.

Topics

1. Predicate logic (Reynolds 1)
2. A Simple Imperative Language (Reynolds 2)
3. Program Specifications and Their Proofs (Reynolds 3)
4. Failure, I/O, Continuations (Reynolds 5)
5. Transition semantics (Reynolds 6)
6. Nondeterminism and Guarded Commands (Reynolds 7)
7. The Lambda Calculus (Reynolds 10; Pierce 4)
8. Simple Types (Reynolds 15.1-15.6; Harper 1-3; Pierce 6, 7)
9. Recursive Types (Reynolds 15.7; Harper 5, 6)
10. An Eager Functional Language (Reynolds 11; Harper 14)
11. First-class Continuations (Reynolds 12; Harper 15)
12. ISWIM-like Languages (Reynolds 13; Harper 16, 17)
13. Normal Order Languages (Reynolds 14)
14. Polymorphism (Reynolds 17; Harper 7; Pierce 12)
15. Existential Types, Data Abstraction, Modules (Reynolds 18; Harper 8, 10; Pierce 13)
16. Subtyping (Reynolds 16)
17. Bounded and F-bounded quantification