CS 411:  Programming Languages

Fall 2003

Greg Morrisett



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.


CS312 or permission of the instructor.



Mon, 1
[pdfIntroduction, Small-step semantics
2Wed, 3[pdfInductive proofs, Large-step semanticsHW1
4Mon, 8[pdfIMP and its small-step semantics
5Wed, 10[pdfEquivalence of small- and large-step semantics, Denotational semanticsHW2
7Mon, 15[pdfProgram analysis as non-standard denotational semanticsHW3
10Mon, 22[pdfIntroduction to axiomatic semantics
11Wed, 24[pdf] An example proof using the Hoare RulesHW4
12Fri, 26[pdf] Weakest (Liberal) Pre-conditions and PCC 
13Mon, 29[pdf] The Untyped Lambda Calculus 
Fri, 3
[pdf] The Simply Typed Lambda Calculus 
16Mon, 6 Logic Programming I (ppt) 
17Wed, 8Logic Programming II (ppt) 
18Fri, 10Logic Programming III (ppt) 
19Mon, 20[pdf] More on the Simply Typed Lambda CalculusHW5
21Fri, 24[pdf] Intro to Polymorphism & Subtyping 
Mon, 10
[pdf] Parametric Polymorphism, RefsHW6
23Wed, 12[pdf] Exceptions 
25Mon, 17[pdf] ContinuationsHW7
26Wed, 19[pdf] Environments and Closures 
28Mon, 24[pdf] Allocation and Garbage Collection 
29Mon, 31[pdf] Overview of Objects and Classes 


  1. See lecture notes for Wed, Sept. 3rd
  2. See lecture notes for Wed, Sept. 10th
  3. See lecture notes for Mon. Sept. 15th
  4. See lecture notes for Wed. Sept. 24th
  5. See lecture notes for Mon. Oct. 20th [solutions]
  6. See lecture notes for Mon. Nov 10th [solutions]
  7. 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.  

For more information on Proof Carrying Code, see George Necula's PCC page.

Course Software:

SML and SML/NJ Documentation:

Interesting papers: