# Computer Science 732: Type Systems for Programming
Languages (Fall 2011)

## Description

This course will serve as an introduction to modern type theory of
programming languages. We will develop types systems for the lambda
calculus and extensions. This will demonstrate the basis for type
systems for high-level functional and object-oriented languages.

The textbook will be ``Types and
Programming Languages'' by Benjamin Pierce of the University of
Pennsylvania (MIT Press).

The course will involve writing proofs in
SASyLF, system for checking proofs
written in a stylized natural language syntax.

The student should be familiar with programming in functional
languages and should have an intuitive sense of the nature of parsing.
The student should also be familiar with proof techniques in discrete
mathematics, and should be able to write inductive proofs over
structures such as trees. The formal prereq is CompSci 431.
Please see the instructor if you are unsure whether you meet the
prerequisite.

### Announcements

- CompSci 654 is not required for this course.

### Handouts

- The syllabus in HTML or Postscript.
- Homework #1 in HTML,
PDF.
- Homework #2 in HTML,
PDF
- Homework #3 in HTML,
PDF.
- Homework #4 in HTML,
PDF.
- Homework #5 in HTML,
PDF.
- Homework #6 in HTML,
PDF.
- Homework #7 in HTML,
PDF.
- Homework #8 in HTML,
PDF.
- Homework #9 in HTML,
PDF.
- Homework #10 in HTML,
PDF.
- Homework #11 in HTML,
PDF.
- Homework #12 in HTML,
PDF.
- Homework #13 in HTML,
PDF.

### Reference

OCaml can be downloaded for free.
The OCaml manual
is available on line. It is also available in
PDF.

Postscript is a trademark of Adobe Systems, Inc.

Last modified: August 29, 2011

boyland@cs.uwm.edu