IndexAnnouncements
Instructor Contact Info
Course Description
Course Textbooks and References
Course Policies
Course Blog
Handouts
Sample Code
Programming in SML
Announcements/Updates
The first class will be on Monday, March 26, 2007 at 10:30am in Ryerson 277.There will be no class on Wednesday and Friday of that week (3/28,30) because I will be away from campus at the ESOP 07 conference in Portugal. I plan to hold makeup classes later in the quarter.
Instructor Contact Info
Name Role Office Office hours Phone David MacQueen Professor Hinds 045 By appointment 2-4980 dbm@cs.uchicago.edu Course Description
This is a graduate seminar on the topic of how to implement modern type and module systems, such as those incorporated in languages like ML and Haskell, as well as type systems employed in the typed intermediate languages used in compilers (e.g. FLINT in SML/NJ). The course work will consist of a mixture of readings from the research literature and programming exercises and projects that will explore implementation ideas and techniques. The type and module system implementation used in the SML/NJ compiler will provide one major example that will be explored in some detail. Readings and student projects will explore other systems such as Haskell and OCaml, and speciallized topics such as local type inference, object-oriented type systems, and advanced record systems.
Programming exercises will be written in Standard ML (SML), so some prior experience with that language would be very helpful.
A tentative, preliminary outline of the course is available here.
Course References
There will be no textbook for the course. Readings will be from a set of papers from the literature, notes and implementation documentation, and source code of implementations such as SML/NJ.There are a couple of books that will be particularly helpful, however, as background reading and references. One is Benjamin Pierce's Types in Programming Languages, which provides a fairly comprehensive introduction to the topic of type systems. For ML programming, I recommend Larry Paulson's ML for the Working Programmer (2nd Edition). There are also a number of useful on-line tutorials as well -- consult the tutorial list at www.smlnj.org.
Programming
The default working language for the course will be Standard ML, which will be used for programming exercises and projects. We will be using the SML/NJ compiler for Standard ML. There are several good sources of documentation and tutorials for SML/NJ available online, and some of these are given in the course SML/NJ page. Additional information and resources for programming in Haskell will appear here shortly.
Course Policies
- Grading will be based on a course paper/project that will be due at the end of the course. There will be no midterm or final exams.
Course Blog
A course blog will be created for announcements and discussions.Handouts and Papers
- A Formulation of the Simple Theory of Types by Alonzo Church (The Journal of Symbolic Logic, Vol 5, No. 2, June, 1940). This is the original definition of the simply typed lambda calculus.
- Stratified Systems of Logic by M. H. A. Newman (Cambridge Philosophical Society, 1942!). This is perhaps the first published account of a type checking algorithm.
- A Theory of Type Polymorphism in Programming by Robin Milner (JCSS 17, 1978).
- Proofs about a folklore let-polymorphic type inference algorithm by Oukseh Lee and Kwangkeun Yi (ACM TOPLAS, 20:4, July 1998).
- Basic Polymorphic Typechecking by Luca Cardelli (Science of Computer Programming, 1988)
- Extension of ML type system with a sorted equational theory on types by Didier R\'emy (INRIA Report No. 1766, 1992)
Sample Code
This section will provide various pieces of sample code.
Resources and Links
This section will provide links to relevant papers and resources on the web.
Dave MacQueen Last modified: Mon Apr 2 17:12:34 CDT 2007