Computer Science 657-3/790-3: Type Systems for Programming Languages (Fall 2003)

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 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 417. Please see the instructor if you are unsure whether you meet the prerequisites.

Announcements

• If/When you copy over the files in the arith directory to do the homework, don't forget the .depend file. An easy fix should you forget:

  touch .depend
  make depend
  

  Then you can make to get the evaluation engine f
• The ocaml binary installed on the grids/miller was broken. I fixed it 8:45pm, 2003/9/2.
• The homework handout was mistakenly an old version; see the web page for the up-to-date version.

Handouts

• The syllabus in HTML or Postscript.
• Homework #1 in HTML or Postscript.
• Homework #2 in HTML or Postscript.
• Homework #3 in HTML or Postscript.
• Homework #4 in HTML or Postscript.
• Homework #5 in HTML or Postscript.
• Homework #6 in HTML or Postscript.
• Homework #7 in HTML or Postscript.
• Homework #8 in HTML or Postscript.
• Homework #9 in HTML or Postscript.
• Homework #10 in HTML or Postscript.
• Homework #11 in HTML or Postscript.

Reference

The OCaml manual is available on line. It is also available in Postscript.

Postscript is a trademark of Adobe Systems, Inc.

Last modified: September 10, 2003