John Boyland
| Instructor | John Boyland |
| Office | 925 EMS, 229-6986 |
| Office Hours | T 2-3pm, R 10am-noon, F 8:30-9:30am, 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. Students will learn how to prove type system properties using a mechanical proof system. Finally graduate students will get a taste of how type-system research progresses.
The participants must have knowledge of programming languages, especially functional languages, logic languages and semantics. Thus CompSci 431 is a prerequisite. Homework will include assignments writing mathematical proofs using SaSyLF.
The required textbook for the course is
Pierce, Types and Programming Languages, MIT Press, 2002.
All work that you submit for this class must be your own work. If you obtained help from anyone or from any reference on paper or on line, you must cite the source and explain the dependence. The only exceptions are the textbook, the course website and the instructor himself. All other help must be acknowledged. Failure to do so may lead to failing the course or even being dismissed from the University.
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 & Pattern Matching | Ch. 1, 2 |
| 9/13 | Terms & Proofs | Ch. 3.0-3 |
| 9/20 | Evaluation | Ch. 3.4-6 |
| 9/27 | Lambda Calculus | Ch. 5 |
| 10/4 | Typing Intro | Ch. 8 |
| 10/11 | Simple Typing | Ch. 9, 10 |
| 10/18 | Simple Extensions | Ch. 11 |
| 10/25 | References | Ch. 13 |
| 11/1 | Subtyping | Ch. 15, 16 |
| 11/8 | Objects | Ch. 18 |
| 11/15 | Recursive Types | Ch. 20, 21 |
| 11/22 | Type Inference | Ch. 22 |
| 11/29 | Universal & Existential Types | Ch. 23, 24 |
| 12/6 | Bounded Quantification | Ch. 26, 27 |
| 12/13 | Type Operators & Kinding | Ch. 29, 30 |
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 root directory of your volume has some special subdirectories:
summary 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.
SaSyLF is available on weise/miller with the proof checker in
/afs/cs.uwm.edu/users/classes/cs732/bin/sasylf.
You can download the latest version from sasylf.org.
OCaml is available on weise/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. Please also be aware of the standard University policies:
http://www.uwm.edu/Dept/SecU/SyllabusLinks.pdf