CSCI  B522  Programming Language Foundations  (Fall 2009)


Course Information

Time & Place

Classes meet on Tuesday and Thursday, 11:15am to 12:45pm in Lindley Hall 115.


Amal Ahmed
Office: Lindley 301G
Phone: 855-4579
Email: amal at
Office hours: Monday 2-3pm, Thursday 2-3pm

Associate Instructor

Nilesh Mahajan
Email: nnmahaja at
Office hours: Wednesday 2-3pm in Lindley 230A

Course Description

Programming languages are a fundamental part of computer science. This course introduces the formal tools needed to describe precisely what a program means. These tools help us answer many useful questions about program analyses and transformations, such as: Topics include:


This course is aimed at Masters students, beginning PhD students, and high-level undergraduates in computer science with a keen interest in the theory and design of programming languages. The only requirement for the course is a considerable degree of mathematical maturity as obtained, for instance, through rigorous undergraduate coursework in discrete mathematics, algorithms and elementary logic. Familiarity with a higher-order functional programming language (e.g., Scheme, ML, Haskell, etc.) would be useful but is not required.


There is one required text for B522: The following book is recommended but not required:

These books are excellent sources for the course, so purchasing them is a good idea. If you don't have a copy, IU library has an electronic version of Pierce that can be accessed by searching the IU catalog and providing your username and passphrase. Winskel will be on reserve at Swain Library.

Some other useful texts that provide a different perspective or more depth in some areas are:


There will be an in-class midterm exam on Thursday, Oct 22nd.

There will be a 24-hour take-home final examination during the exam period at the end of the semester.


There will be 6 homework assignments during the course of the semester. Assignments will typically be made available on Thursdays and will be due back the following Thursday.

If a significant percentage of the class does poorly on one or more problems on the homework, the instructor may reassign those problems. Such assignments to redo a specific part of a homework will typically be announced on a Tuesday. You will have two days to submit a revised solution (due back by midnight on the due date). The score obtained on the revised solution will replace the earlier score received for that problem. This policy is aimed at ensuring that the emphasis is properly on learning the course material, and not on simply "getting through" the assignments. Note that due dates for homework revisions are marked with an "r" suffix on the schedule (e.g., hw1r).

All homeworks are due by 3pm on the due date unless otherwise specified. Extensions are granted only in extenuating circumstances at the discretion of the instructor. All written assignments must be typeset (using LaTeX) in the interest of legibility. Instructions for submitting a programming assignment will be given with the assignment.

Academic Integrity

You are responsible for reading the departmental statement on academic integrity before starting the first homework.

Unless explicitly instructed otherwise, all homework and exam work is to be solely your own, and may not be shared with or borrowed from any other person in the course. You are not permitted to draw upon assignments or solutions from similar instances of the course, nor to use course materials (such as assignments or programs) obtained from any web site or other external source in preparing your work.

You are encouraged to discuss homework assignments with other students in the class, but you must adhere to the whiteboard policy. At the end of the discussion the whiteboard must be erased and you must not transcribe or take with you anything that has been written on the board (or elsewhere) during your discussion. You must be able to reproduce the results solely on your own after any such discussion.

Grading Policy

The final grade will be comprised of homework (60%), midterm exam (15%) and final exam (25%) scores.


LaTeX Help

Homework Templates

OCaml Resources

Course Schedule

(Subject to change)

# Date Topics Readings* Lecture Notes out in

Operational semantics and proof techniques

Sep 1 No class P1,2
1 3 Introduction; Lambda calculus P3 syllabus, lecture1
2 8 Structural Operational Semantics, CBV vs. CBN, recursion P5 lecture2
3 10 Lambda calculus encodings, equivalence, reduction, normal forms P5.2 lecture3 hw1
4 15 OCaml tutorial (Roshan James)
5 17 IMP introduction W2 lecture5 hw1
6 22 IMP small-step and big-step SOS hw1r
7 24 Inductive definitions, well-founded induction, rule induction P3.2,3.3, W3,4 lecture7 hw2   code hw1r
8 29 Evaluation contexts, semantics by translation lecture8

Language features and translations

9 Oct 1 uML and strong typing lecture9 exerciseA hw2
10 6 uML; Run-time type checking hw2r
11 8 Naming and scope; Modules lecture11 hw3 hw2r
12 13 State and mutable variables lecture12
13 15 Translation from uML+references to uML hw3
14 20 Continuation-passing style, CPS conversion lecture14
22 Midterm (in class) hw3r

Static semantics (type systems)

15 27 Midterm discussion
16 29 Simply-typed lambda-calculus P8.1,8.2,9.1,9.2 hw4 hw3r
17 Nov 3 Type safety P8.3,9.3-9.5
18 5 Products, sums, recursion and more P11 hw5 hw4
19 10 References P13 hw4r
20 12 Exceptions P14 hw4r
21 17 Subtyping P15.1-15.6 hw5
22 19 Recursive types P20 lecture22 hw6
23 24 Parametric polymorphism P23
26 No class: thanksgiving break
24 Dec 1 Propositions as types Wadler, P9.4 lecture24 hw5r
25 3 Strong normalization and logical relations P12 lecture25 hw6
26 8 Existential types P24 hw6r hw5r
27 10 Object-oriented features, object encodings P18 hw6r

Key to Readings

P = Pierce, W = Winskel

Amal Ahmed
Last modified: Tue Dec 8 18:32:55 EST 2009

Valid XHTML 1.0!