**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: