| Instructor: | John Tang Boyland |
| Place: | EMS E295 |
| Time: | TR 5:30-6:455pm |
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 a moderate amount of programming, probably in The OCaml dialect of ML, as well as some written homework assignments with a more mathematical bent.
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 prereqs are CompSci 431 and 654. Please see the instructor if you are unsure whether you meet the prerequisites.
Then you can make to get the evaluation engine ftouch .depend make depend
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: September 2, 2005
boyland@cs.uwm.edu