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

Instructor:John Tang Boyland
Place:PHY 145
Time:TR 4:00-5:15pm


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.




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