Semantics of Programming Languages Course #: COMP 411 

As computer programs play an increasingly more significant role in our daily lives, knowing what they are supposed to be doing and its relation what they actually do becomes particularly important. For example, given two programs we might want ask: are they equivalent? If we optimize, compile, or even write programs, this fundamental question comes up. Often, we rely on intuition for answering this question. But in critical applications where avoiding programming errors is important, or if we just want to produce higher quality software, there is a need for more rigorous techniques to answer this question. The idea is that the less we rely on intuition and replace by analytical methods, the more reliable the resulting software systems can be. The goal of this course is to introduce you to some mathematical tools that can help you to do this. Collectively, they are called formal semantics.
The course will focus on operational semantics and type systems. These tools will be applied to a wide range of programming languages, including imperative, nondeterministic, parallel (or concurrent), as well as functional programming languages. Features such as strictness, laziness, recursion and recursive datatypes will also be covered. The course will follow closely the textbook Types and Programming Languages by Benjamin Pierce.
Course work will include reading the text book, solving homework problems (40%), a midterm (20%), and a final (30%). Homework problems are assigned each Monday, cover material up to Wedensday, and are due by Friday. Timeliness, attendance and preparedness for class are required and are evaluated by quizes (10%). Homeworks must be submitted as plain text, by email, and before class on the due date. Late submissions are not accepted except in extraordinary circumstances, and must be by arranged before the original deadline.
Students are encouraged to discuss the material covered in class in homeworks on class mailing list (comp411L). Please make sure you subscribe to this list, as any important announcements to the class will be posted there.
# 
Date 
Day 
Topic 
Homework (due this day) 
Comments 
1 
1/12/05 
W  Organization. Introduction to types and programming languages (Ch 1)[notes] 

2 
1/14/05  F  Mathematical preliminaries (Ch 2) [notes] 

1/17/05  M  No class today (MLK) 

3 
1/19/05  W  Untyped arithmetic expressions (Ch 3) Denotational sem. [notes] 
2.2.{6,7,8}. Download and install OCaml. Implement factorial, Fibonacci, and Ackermann, and hand them in. Prove L  e <=> FV(e) ⊆ L (see 1/14 notes) 

4 
1/21/05  F  (Ch 3 cont'd) Big and smallstep sem. [notes] 

5 
1/24/05  M  (Ch 3 cont'd) Relating big and smallstep sem. [notes] 
3.2.{5,6}. 3.5.{10,13}. Read Ch 4. Download arith. Hand in a list of the types of datastructures and functions used in the code. 4.2.2. Prove properties 14 stated in 1/19 notes. 

6 
1/26/05  W  The untyped lambda calculus (Ch 5) [notes]  
7 
1/28/05  F  Nameless representations of terms (Ch 6) and an implementation of the lambda calculus (Ch 7) [notes] 

8 
1/31/05  M  Typed arithmetic expressions (Ch 8) [notes] 
5.2.{4,10} , 5.3.8. State and prove relation between bigstep and small semantics. State and prove condition for reordering substitions. 6.2.{7,8}, 6.3.{1,2}, prove two substitution statements from 1/28 notes. 

9 
2/2/05  W  Simply typed lambda calculus (Ch 9) [notes] 

10 
2/4/05  F  An implementation of simple types (Ch 10) [notes] 

11 
2/7/05  M  Some simple extensions to simple types (Ch 11.[17]) [notes] 
8.2.3,8.3.{5,6,7,8},9.2.3,9.3.2,9.3.10,9.4.1. Test implementation in Ch 10 using a set of 10 different examples, and hand in output. Prove exchange and weakening lemmas (2/4 notes) 

12 
2/9/05  W  More extensions to simple types (Ch 11.[812]) [notes] 

13 
2/11/05  F  Normalization (Ch 12) [notes] 

14 
2/14/05  M  Adding references to the simply typed lambda calculus (Ch 13) 
11.5.1, 11.8.2, 11.9.1, 11.11.{1,2} 

15 
2/16/05  W  Adding exceptions (Ch 14) [notes] 

16 
2/18/05  F  Subtyping basics (Ch 15.[14]) [notes] 

17 
2/21/05  M  Subtyping and interaction with other features (Ch 15.[58]) [notes] 
11.12.1, 13.4.1, 13.5.{2,8}, 14.3.1, 15.2.{2,3,4,5}, 15.5.1. Where results are listed, write up a proof independently of what is writen in the text. 

18 
2/23/05  W  Some metatheoretic properties of subtyping (Ch 16) [notes] 

19 
2/25/05  F  An implementation of subtyping (Ch 17) [notes] 

20 
2/28/05  M  Subtyping (Ch 17) [notes] 
16.2.{1,3,5,6}, 16.3.{2,3,4}, 16.4.1, 17.3.{1,2,3,4} 

21 
3/2/05  W  Imperative objects (Ch 18.[16]) [notes] 

22 
3/4/05  F  Imperative objects (Ch 18.[614]) [notes] 

3/7/05  M  
3/9/05  W  
3/11/05  F  
23 
3/14/05  M  Featherweight Java (Ch 19) [notes]  No homework this week  
24 
3/16/05  W  Featherweight Java (Ch 19) [notes] 

25 
3/18/05  F  Featherweight Java (Ch 19) [notes] 

26 
3/21/05  M  Featherweight Java (Ch 19) [notes] 
19.4.{3,4,6}  
27 
3/23/05  W  Recursive types (Ch 20) [notes] 


28 
3/25/05  F  Recursive types (Ch 20) [notes] 

29 
3/28/05  M  Metatheoretic properties of recursive types (Ch 21) [notes] 
type the Ycombinator (3/25 notes)  
30 
3/30/05  W  Metatheoretic properties of recursive types (Ch 21) [Covered only briefly this year] [notes] 

31 
4/1/05  F  [Class to be rescheduled] 

32 
4/4/05  M  Type reconstruction (Ch 22) [notes] 
20.1.{1,2,3,4,5} 

33 
4/6/05  W  Type reconstruction and Constraintbased Typing (Ch 22) [notes] 

4/8/05  F  
34 
4/11/05  M  Type Reconstruction and Constraintbased Typing [notes] 
22.2.3, 22.3.{3,9,10,11} 

35 
4/13/05  W  Type Reconstruction and Unification [notes] 

36 
4/15/05  F  Type reconstruction and Unification (Ch 22) [notes] 

37 
4/18/05  M  Type reconstruction and Unification (Ch 22) [notes] 
22.3.{9,10,11}, 22.4.{3,6} , 22.5.2  
38 
4/20/05  W  Universal types basics (Ch 23.[16]) [notes] 

39 
4/22/05  F  Universal types basics (Ch 23.[16]) [notes] 

40 
4/25/05  M  Universal types basics (Ch 23.[16]) [notes] Existential types (Ch 24) [notes] [notes] 
23.4.{3,5,6,8,9}, 23.5.{1,2} 

41 
4/27/05  W  Higherorder polymorphism (Ch 29, Ch 30.[13]) [notes]  24.1.1, 24.2.1, 24.2.2, 24.2.3 

42  4/29/05  F  Higherorder polymorphism (Ch 29, Ch 30.[13]) [notes] 
29.1.1, 29.1.2 
Students with disabilities are encouraged to contact me during the first two weeks of class regarding any special needs. Students with disabilities should also contact Disabled Student Services in the Ley Student Center and the Rice Disability Support Services.