John Boyland
| Instructor | John Boyland |
| Office | 925 EMS, 229-6986 |
| Office Hours | T 1-2pm, R 9-11am, or by appt. |
| Course Homepage | http://www.cs.uwm.edu/classes/cs732 |
Most programming languages distinguish between different uses of the bits processed by the computer, some are treated as numbers, others as strings of characters, yet others as arrays, records, objects, files, documents or data bases. Type theory is the study of how these distinctions can be made and what they can mean. This course starts with the simplest programming language: the lambda calculus, and shows how types can be imposed on it. Extensions will be made to the lambda calculus in order to capture the essence of types systems used in modern programming languages.
It is the intention that this course bring a large array of programming language research within the grasp of the participant. In particular, the participant should become fluent in current notation and learn to read definitions of type systems, both proof systems and algorithmic type systems. Finally, it is expected that participants will get a taste of how type theory research progresses.
The participants must have knowledge of programming languages and compilers. Thus both CompSci 431 and 654 are strongly recommended prerequisites. Homework will include assignments in the OCaml dialect of ML and also mathematical proofs.
The required textbook for the course is
Pierce, Types and Programming Languages, MIT Press, 2002.
The grade for the course will be computed from the following parts:
The following schedule is subject to change as time is needed to cover the material.
| Week starting | Topic | Reading |
|---|---|---|
| 9/6 | Introduction | Ch. 1, 2, 3, 4 |
| 9/13 | Lambda Calculus I | Ch. 5 |
| 9/20 | Lambda Calculus II | Ch. 6, 7 |
| 9/27 | Typing Intro | Ch. 8 |
| 10/4 | Simple Typing | Ch. 9, 10 |
| 10/11 | Simple Extensions | Ch. 11 |
| 10/18 | References, Exceptions | Ch. 13, 14 |
| 10/25 | Subtyping | Ch. 15, 16, 17 |
| 11/1 | Objects | Ch. 18, (19) |
| 11/8 | Recursive Types | Ch. 20, 21 |
| 11/15 | Type Inference | Ch. 22 |
| 11/22 | Universal & Existential Types | Ch. 23, 24, (25) |
| 11/29 | Bounded Quantification | Ch. 26, 27 |
| 12/5 | Type Operators & Kinding | Ch. 29, 30 |
| 12/12 | Higher-Order Polymorphism and Objects | Ch. 31, notes |
All your programming work should be done in the AFS volume assigned to you. The absolute pathname is
/afs/cs.uwm.edu/users/classes/cs732/001/PantherID.
We recommend that you make a symbolic link from your UNIX home
directory to this directory.
Before you can access this directory, you will need to obtain
authenticate yourself to AFS using Kerberos. This can be done using
/usr/afsws/bin/klog PantherID
and type your Kerberos password. The kpasswd.uwmcs command in the
same directory can be used to change your kerberos password.
(The command kpasswd won't work. One version of this command
simply will claim that you didn't type the old password correctly. The
other will change your password but will make it impossible to 'klog'.)
The root directory of your volume has some special subdirectories:
summary.txt lists all the scores and
computes the weighted percentage.The file system is a distributed network filesystem that permits you to do your homework on your home computer once you have installed Open AFS.
OCaml is available on miller with executables in
/afs/cs.uwm.edu/users/classes/cs732/ocaml/bin:
ocaml is an interactive system and ocamlc is a
compiler. These executables need to be put in your path so you can
use them.
The OCaml manual
is available from the class web page.
If you would like to install OCaml on your home machine, see
http://caml.inria.fr.
The implementations described in the textbook are in
/afs/cs.uwm.edu/users/classes/cs732/checkers.
These implementations come with makefiles that show how they work.
If you will be needing accomodations in order to meet any of the requirements of this course, please contact the instructor as soon as possible.