CS 411: Programming Languages
Fall 2003
Announcements:
Overview:
An introduction to semantics, models, design,
and implementation of programming languages. Topics include operational and
denotational semantics, type systems, parameter passing, higher-order functions,
dynamic vs. lexical scope, lambda calculus, laziness, exceptions, side effects,
continuations, objects, and modules.
Prerequisites:
CS312 or permission of the instructor.
Logistics:
- Meetings: Classes are held Monday, Wednesday,
and Friday from 10:10am to 11:00am in 1120 Snee Hall.
- Book: Concepts in Programming Languages,
John C. Mitchell, Cambridge University Press, 2003. ISBN 0 521 78098
5. We will also be using notes from Robert Harper of Carnegie Mellon
University (to be handed out in class.)
- TA: Jed
Liu
- Office Hours: Morrisett: Monday,
11am-12pm, Upson 4133; Liu: Monday, 3-4pm, Upson 5157 or by appointment.
- Newsgroup: cornell.class.cs411
- Exams: Midterm: (in class) Oct. 31, Final:
(in class) Dec. 5
- Grading: Midterm (20%), Final (25%),
Homework (50%), Participation (5%)
Lectures:
| # | Date | Topic | HW |
| 1 | September
Mon, 1 | [pdf] Introduction, Small-step semantics |
| 2 | Wed, 3 | [pdf] Inductive proofs, Large-step semantics | HW1 |
| 4 | Mon, 8 | [pdf] IMP and its small-step semantics |
| 5 | Wed, 10 | [pdf] Equivalence of small- and large-step semantics, Denotational semantics | HW2 |
| 7 | Mon, 15 | [pdf] Program analysis as non-standard denotational semantics | HW3 |
| 10 | Mon, 22 | [pdf] Introduction to axiomatic semantics |
| 11 | Wed, 24 | [pdf] An
example proof using the Hoare Rules | HW4 |
| 12 | Fri, 26 | [pdf] Weakest
(Liberal) Pre-conditions and PCC | |
| 13 | Mon, 29 | [pdf] The
Untyped Lambda Calculus | |
| 15 | October
Fri, 3 | [pdf] The Simply Typed Lambda
Calculus | |
| 16 | Mon, 6 | Logic
Programming I (ppt) | |
| 17 | Wed, 8 | Logic
Programming II (ppt) | |
| 18 | Fri, 10 | Logic
Programming III (ppt) | |
| 19 | Mon, 20 | [pdf] More
on the Simply Typed Lambda Calculus | HW5 |
| 21 | Fri, 24 | [pdf] Intro
to Polymorphism & Subtyping | |
| 22 | November
Mon, 10 | [pdf] Parametric Polymorphism, Refs | HW6 |
| 23 | Wed, 12 | [pdf] Exceptions | |
| 25 | Mon, 17 | [pdf] Continuations | HW7 |
| 26 | Wed, 19 | [pdf] Environments
and Closures | |
| 28 | Mon, 24 | [pdf] Allocation
and Garbage Collection | |
| 29 | Mon, 31 | [pdf] Overview
of Objects and Classes | |
Homework:
- See lecture notes for Wed, Sept. 3rd
- See lecture notes for Wed, Sept. 10th
- See lecture notes for Mon. Sept. 15th
- See lecture notes for Wed. Sept. 24th
- See lecture notes for Mon. Oct. 20th [solutions]
- See lecture notes for Mon. Nov 10th [solutions]
- See lecture notes for Mon. Nov 17th.
Information and Resources:
Other Texts:
These books are available in the engineering library. The Winskel book
is something that I recommend looking at for additional material on operational,
denotational, and axiomatic semantics. In fact, the material in the notes
is drawn largely from this book.
- The Formal Semantics of Programming Languages, Glynn Winskel, MIT
Press.
- The Science of Programming, David Gries.
For more information on Proof Carrying Code, see George Necula's PCC
page.
Course Software:
SML and SML/NJ Documentation:
Interesting papers: