CMSC 336: Type Systems for Programming Languages

Winter Quarter, 2002
Tuesdays and Thursdays, 1:30 - 2:50 pm
Ryerson 276

Index

Announcements
Instructor Contact Info
Course Description
Course Textbook
Course Policies
Course Schedule
Course Homework Exercises
Additional Useful Links
Programming in SML

Announcements/Updates

The first class will be on 3rd January, 2002 at 1:30pm in Ry 276.
There will be a makeup class (for 1/18/02) on Friday 2/1/02 from noon to 1:30pm in Room 257.

Instructor Contact Info

Name	Role	Office	Office hours	Phone	Email
David MacQueen	Professor	Ryerson 256	Tue, Thu: 3:30-5:00pm	(773) 702-4980	dbm@cs.uchicago.edu

Course Description

Type systems are formal systems or languages for describing the structure of data and program interfaces. They are of immense practical utility because they provide a valuable though weak form of program specification that can be automatically checked by compilers. Extensive research in the area of type systems has also contributed to our basic understanding of the architecture and meaning of programming languages.

The use of type systems in the design and analysis of languages has been particularly successful for functional and object-oriented languages, so most of the language examples will be taken from these families of languages.

This course will cover the basic ideas of type systems, their formal properties, their role in programming language design and their implementation. Exercises involving design and implementation will explore the various options and issues.

Course Textbook

We will use the following textbook: Types and Programming Languages by Benjamin C. Pierce.

Almost all the material covered in the course is included in this text book. The lecture slides will also be made available as PowerPoint and postscript or pdf documents.

The textbook will be published by the second half of January. Meanwhile, the first 11 chapters of the book are available in this postscript file.

Course Policies

Grading will be (tentatively) based on the following:

Assignments: 20%
Project: 30%
Final: 40%

Assigments: There will be six assignments each of 5% weight. The assignments will be due a week after they are given, with a 20% penalty for late submissions (maximum of 2 days).
Collaboration: As in most courses, we encourage students to discuss course material among themselves. Discussions of assignment problems is also permitted to an extent, but submitted assignments should be your own work, and collaborative discussions should be acknowledged.
Examination Date: Tentatively, the final examination will be on 3/??.

Course Schedule

Here is a tenative, and probably overly ambitious, schedule of the lectures. This is subject to continual adjustment, of course.

Lecture Date Topic Reading Slides Code

0 1/03 Introduction, overview, history, administration 1, (2) ppt,pdf

1 1/08 Preliminaries: syntax, operational semantics 3,4 ppt,pdf arith.tgz

2 1/10 Introduction to the lambda-calculus 5.1,5.2 ppt,pdf

3 1/15 Formalizing the lambda-calculus 5.3, 6, 7 ppt,pdf untyped.tgz

4 1/22 Types; the simply typed lambda-calculus 8,9,10 ppt,pdf tyarith.tgz
simplebool.tgz

5 1/24 Simple extensions; derived forms 11 ppt,pdf letexercise.tgz

6 1/24 More extensions 11

7 1/29 References 13

8 1/31 Subtyping 15

9 2/05 Metatheory of subtyping 16,17

10 2/07 Imperative objects 18 ppt,pdf

11 2/12 Recursive types 20

12 2/14 Metatheory of recursive types 21 ppt,pdf

13 2/26 Type reconstruction 22 ppt,pdf

14 3/1 Universal polymorphism 23 ppt,pdf

15 3/1 Existential polymorphism; ADTs 24, (25) ppt,pdf

16 3/7 Bounded quantification; objects 26, 27

17 3/05 Type operators; F-omega 29,30

3/14 Final Exam

Lecture	Date	Topic	Reading	Slides	Code
0	1/03	Introduction, overview, history, administration	1, (2)	ppt,pdf
1	1/08	Preliminaries: syntax, operational semantics	3,4	ppt,pdf	arith.tgz
2	1/10	Introduction to the lambda-calculus	5.1,5.2	ppt,pdf
3	1/15	Formalizing the lambda-calculus	5.3, 6, 7	ppt,pdf	untyped.tgz
4	1/22	Types; the simply typed lambda-calculus	8,9,10	ppt,pdf	tyarith.tgz simplebool.tgz
5	1/24	Simple extensions; derived forms	11	ppt,pdf	letexercise.tgz
6	1/24	More extensions	11
7	1/29	References	13
8	1/31	Subtyping	15
9	2/05	Metatheory of subtyping	16,17
10	2/07	Imperative objects	18	ppt,pdf
11	2/12	Recursive types	20
12	2/14	Metatheory of recursive types	21	ppt,pdf
13	2/26	Type reconstruction	22	ppt,pdf
14	3/1	Universal polymorphism	23	ppt,pdf
15	3/1	Existential polymorphism; ADTs	24, (25)	ppt,pdf
16	3/7	Bounded quantification; objects	26, 27
17	3/05	Type operators; F-omega	29,30
	3/14	Final Exam

Additional Useful Links

Documentation and software for Standard ML of New Jersey (SML/NJ) are available at www.smlnj.org.