Semantics of Programming Languages

Course #:  COMP 411
Instructor:  Walid Taha (DH 3103)
Class time:  MWF 10:00AM 10:50AM (Office Hours:  M 2:00PM 2:50PM)
Class room: DH 1042

 
   

Introduction

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, non-deterministic, 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 (comp-411-L). Please make sure you subscribe to this list, as any important announcements to the class will be posted there.

Lectures

#

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 small-step sem. [notes]

   

5

 1/24/05  M

(Ch 3 cont'd) Relating big and small-step sem. [notes]

 3.2.{5,6}.  3.5.{10,13}.  Read Ch 4. Download arith.  Hand in a list of the types of data-structures and functions used in the code.  4.2.2. Prove properties 1-4 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 big-step 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.[1-7]) [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.[8-12]) [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.[1-4]) [notes]

   

17

 2/21/05  M

Subtyping and interaction with other features (Ch 15.[5-8]) [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.[1-6]) [notes]

   

22

 3/4/05  F

Imperative objects (Ch 18.[6-14]) [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 Y-combinator (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 Constraint-based Typing (Ch 22)  [notes]

   
 4/8/05  F      

34

 4/11/05  M

Type Reconstruction and Constraint-based 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.[1-6])  [notes]

   

39

 4/22/05  F

Universal types basics (Ch 23.[1-6])  [notes]

   

40

 4/25/05  M

Universal types basics (Ch 23.[1-6]) [notes] Existential types (Ch 24)  [notes]  [notes]

  23.4.{3,5,6,8,9}, 23.5.{1,2}

 

41

 4/27/05  W Higher-order polymorphism (Ch 29, Ch 30.[1-3])  [notes]

  24.1.1, 24.2.1, 24.2.2, 24.2.3

 
42  4/29/05  F

Higher-order polymorphism (Ch 29, Ch 30.[1-3])  [notes]

  29.1.1, 29.1.2

 

Additional References

Accommodations for Students with Special Needs

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.