CMSC 336: Type Systems for Programming Languages

Winter Quarter, 2005 
Tuesdays and Thursdays, 9:00 - 10:20 am
Ryerson 276

Index

Announcements
Instructor Contact Info
Course Description
Course Textbook
Course Policies
Course Mailing List
Course Handouts
Course Schedule
Course Homework Exercises
Course Project
Additional Useful Links
Programming in SML

Announcements/Updates

Instructor Contact Info

Name Role Office Office hours Phone Email
David MacQueen Professor Ryerson 256 Tue, Thu: 3:30-5:00pm (773) 702-4980 dbm@cs.uchicago.edu

Course Description

Type systems are formal systems or languages for describing the structure of data and program interfaces. They are of immense practical utility because they provide a valuable though weak form of program specification that can be automatically checked by compilers. Extensive research in the area of type systems has also contributed to our basic understanding of the architecture and meaning of programming languages.

The use of type systems in the design and analysis of languages has been particularly successful for functional and object-oriented languages, so most of the language examples will be taken from these families of languages.

This course will cover the basic ideas of type systems, their formal properties, their role in programming language design and their implementation. Exercises involving design and implementation will explore the various options and issues.

Course Textbook

We will use the following textbook: Types and Programming Languages by Benjamin C. Pierce.

Most of the material covered in the first half of the course is included in this text book. The lecture slides will also be made available as pdf documents. The second half of the course will be based on readings in current research on module systems.

Course Policies

Course Mailing List

A mailing list has been created for the course. The address is cmcs33600@mailman.cs.uchicago.edu. The web page for the mailing list is at http://mailman.cs.uchicago.edu/mailman/listinfo/cmcs33600.

Course Handouts

  • Catalog of basic mathematical terms and notations.

    Course Schedule

    Here is a very tenative, and also inaccurate schedule of the lectures. This will be revised substantially, but it will still be useful for the first few weeks of the course.

    Lecture Date Topic Reading Slides Code
    0 1/4 Introduction, overview, admin; Untyped Arithmatic 1, 2, 3 Lesson0.pdf
    Lesson1.pdf    		  
    1 1/6 Implementing Arith; Untyped lambda-calculus 4, 5 Lesson2.pdf arith.tgz
    source.tgz
    2 1/11 Formalizing, implementing lambda-calculus 5, 6, 7 Lesson3.pdf  
      1/13 No class      
    3 1/18 Types; the simply typed lambda-calculus 8,9,10 Lesson4.pdf tyarith.tgz
    simplebool.tgz
    4 1/20 Simple extensions; derived forms 11 Lesson5.pdf letexercise.tgz
    5 1/25 More extensions 11    
    6 1/27 References 13    
    7 2/1 Subtyping 15    
    8 2/3 Metatheory of subtyping 16,17    
    9 2/8 Imperative objects 18 Lesson8.pdf  
    10 2/10 Recursive types 20    
    11 2/15 Metatheory of recursive types 21 Lesson9.pdf  
    12 2/17 Type reconstruction 22 pdf  
    13 2/22 Universal polymorphism 23 ppt,pdf  
    14 2/24 Existential polymorphism; ADTs 24, (25) ppt,pdf  
    15 3/7 Bounded quantification; objects 26, 27    
    16 3/05 Type operators; F-omega 29,30    

    Additional Useful Links