CS510 Types and Semantics Fall 2005

Instructor: Andrew Tolmach

Course Information

• Syllabus

Course Mailing List

• Visit the cs510types list homepage to subscribe.

Lecture Notes

• Untyped Lambda Calculus (4up)
• Type Inference

Homework Assignments

• Homework 1 (due 10/6/05) Problems 5&6 sample solutions
• Homework 2 (due 10/13/05) Problem 1 sample solution Problem 9 sample solution
• Homework 3 (due 10/20/05) Problem 4 sample solution
• Homework 4 (due 10/27/05) Problem 1 sample solution
• Homework 5 (due TUESDAY 11/8/05)
  • Materials for exceptions exercise in OCAML
  • Problem 6 sample solution
• Homework 6 (due 11/17/05) Problems 3,4,6 sample solutions
• Homework 7 (due 12/1/05) Problems 1,5,9 sample solutions

Textbook Resources

• OCAML code for the various typechecker implementations. (I found it necessary to change "include .depend" to "-include .depend" in the Makefiles to get things started.)
• The author maintains a list of errata for Types and Programming Languages. Check here first if you can't make sense of something in the text.

OCAML Resources

• The OCAML web page.
• You'll definitely want access to the system documentation.
• You can download the latest version for your own machine.
• You may find this tutorial useful; here are pointers to some other on-line documentation.

Latex Resources

• Pierce's style file for typesetting the definitions of inference rules.
• A proof style file which I often use for typesetting derivations.

Interesting Papers to Explore

• Morrisett, Felleisen, and Harper, "Abstract Models of Memory Management," FPCA95.
• Wright and Felleisen, "A Syntactic Approach to Type Soundness", Information and Computation, 115(1), pp. 38-94 (1994).