Type systems are the most widely used formal methods technique. A type system is both a specification used to specify or predict the behaviour of programs, and part of a programming language implementation used to detect violation of that specification (bugs). In this course, we'll learn what type systems are and how to implement type systems.
We aim to cover 10 topics, approximatley 1 per week (with some time spent on
other things).
You are
All the readings for this course are available online and linked to from the course schedule on this page.
This course is intended for graduate students in computer science. There are no formal course prerequisites, but you are expected to have the kind of mathematical maturity typical of one who has taken an undergraduate discrete math or theory of computation course. The course will not involve building any formal models or proofs, but will require learning to read some. The course involves implementing a small programming language, so students with background in programming language implementation, such as CPSC 311 and CPSC 411, will be very familiar with many of the data structure representations and implementation techniques required to implement a type system.
This course is run as a graduate seminar course. Student will read, present, and lead the discussion of selected readings on type systems and type system implementations. Prior to a discussions, students are required to submit a summary and technical critique of the reading. Students will be assigned to lead discussion. The role of the lead is to walk the class through the reading, focusing attention on specific parts of the material that may have been confusing or difficult, finding and bringing to the attention of the group any related context that may help with understanding. Students may be assigned to play the role of skeptic or advocate during discussion, to raise specific benefits or limitations from the reading during discussion.
Students will also complete a semester-long project implementing a type system, which they will present at the end of the course. The type system must include at least 3 fetaures or implementation techniques the readings during the course. The project can be written in any language using any design paradigms, so long as you can explain the design and implementation.
You will receive a 0 on anything you submit that contains any plagarised materials; even a single sentence. Repeated violations will result in failing the course and referral to the university for disciplinary action. I suggest reading the following on plagarism. https://www.carolemieux.com/teaching/academic_honesty.html
One skill you will need or need to learn is how to approach reading scientific research work. You will probably need to read both more and less than is in the list below. You may need to work backwards from these points to find missing background, context, or additional materials. This is common in reading research---an article is rarely completely self contained, and the authors may not even tell you where to find background information. While reading from this list, you should identify questions you have from the reading, background you are missing, and limitations, benefits, or trade-offs in the present work that may not be made explicit. You should try to answer these questions yourself by finding additional reading that provides the answers. You should also feel free to bring these questions, and any additional material you found helpful, to the discussion in-class.
You should not necessarily read all the material, or read in order. If you already are motivated to see the solution the paper describes, skip the intro. If you know the history or limitations of past work, skip the related work. Some parts of an article or chapter may not be relevant---if we're trying to understand an implementation technique, we might skip all the proofs the authors do about their technique and focus only on the algorithms. (Although, proofs and theorems may give you some insight into trade-offs about the implementation.)
| Discussion | 25% |
| Critiques | 25% |
| Project | 50% |
To facilitate discussion among students in the class and myself, we are using the Piazza Q&A platform. The system allows you to ask questions, refine answers as a group, carry on followup discussions, and disseminate relevant information. Rather than emailing questions to me, I ask that you post your questions to Piazza.
Find our class page at http://piazza.com/ubc.ca/winterterm22022/cpsc539b.
The following books are required but accessible online through the library:The following is a draft course schedule, based on a prior offering of the course. The exact details (including some topics) will vary depending on the content covered in class and the interests and needs of the students (and myself).
| # | Date | Topics | Reading | Notes | |
|---|---|---|---|---|---|
| 0 | Mon, Jan 9 | Course Introduction | |||
| 1 | Wed, Jan 11 | PL and Type Theory Basics Notation | |||
| 2 | Fri, Jan 13 23:59 | Preferences for leading discussion due | |||
| 3 | Mon, Jan 16 | NO CLASS; POPL | |||
| 4 | Wed, Jan 18 | NO CLASS; POPL | |||
| 5 | Mon, Jan 23 12:00 | Simple types summary/critique due | |||
| 6 | Mon, Jan 23 | Simple types | TAPL Chapter 9 and Chapter 11 | ||
| 7 | Wed, Jan 25 | Simple types | TAPL Chapter 9 and Chapter 11 | ||
| 8 | Mon, Jan 30 12:00 | Bi-directional summary/critique due | |||
| 9 | Mon, Jan 30 | Bi-directional type checking | http://www.davidchristiansen.dk/tutorials/bidirectional.pdf | ||
| 10 | Wed, Feb 1 | Bi-directional type checking | http://www.davidchristiansen.dk/tutorials/bidirectional.pdf | ||
| 11 | Mon, Feb 6 12:00 | Simple types for effect critique/summary due | |||
| 12 | Mon, Feb 6 | Simple types for effects | TAPL Chapter 13 and Chapter 14 | ||
| 13 | Wed, Feb 8 | Simple types for effects | TAPL Chapter 13 and Chapter 14 | ||
| 14 | Mon, Feb 13 12:00 | Subtyping critique/summary due | |||
| 15 | Mon, Feb 13 | Subtyping | TAPL Chapter 15 and Chapter 16 | TAPL Chapter 18 may also be useful | |
| 16 | Wed, Feb 15 | Subtyping | TAPL Chapter 15 and Chapter 16 | TAPL Chapter 18 may also be useful | |
| 17 | Mon, Feb 20 | NO CLASS; Midterm break! | |||
| 18 | Wed, Feb 22 | NO CLASS; Midterm break! | |||
| 19 | Mon, Feb 27 12:00 | Hindley-Milner Type Inference critique/summary due | |||
| 20 | Mon, Feb 27 | Hindley-Milner Type Inference | TAPL Chapter 22 | ||
| 21 | Wed, Mar 1 | Hindley-Milner Type Inference | TAPL Chapter 22 | ||
| 22 | Mon, Mar 6 12:00 | Typeclasses critique/summary due | |||
| 23 | Mon, Mar 6 | Typeclasses | https://doi.org/10.1145/75277.75283 | ||
| 24 | Wed, Mar 8 | Typeclasses | https://doi.org/10.1145/75277.75283 | ||
| 25 | Mon, Mar 13 12:00 | Typed assembly critique/summary due | |||
| 26 | Mon, Mar 13 | Typed Assembly | Section 7 of https://doi.org/10.1145/319301.319345 | ATAPL Chapter 4 may also be helpful | |
| 27 | Wed, Mar 15 | Typed Assembly | Section 7 of https://doi.org/10.1145/319301.319345 | ATAPL Chapter 4 may also be helpful | |
| 28 | Mon, Mar 20 12:00 | Refinement types critique/summary due | |||
| 29 | Mon, Mar 20 | Refinement Types | https://arxiv.org/abs/2010.07763 | ||
| 30 | Wed, Mar 22 | Refinement Types | https://arxiv.org/abs/2010.07763 | ||
| 31 | Mon, Mar 27 12:00 | Sized types critique/summary due | |||
| 32 | Mon, Mar 27 | Sized Types | https://doi.org/10.1145/237721.240882 | ||
| 33 | Wed, Mar 29 | Dependent types critique/summary due | |||
| 34 | Wed, Mar 29 12:00 | Dependent Types | ATAPL Chapter 2.6 and Section 6 and 7 of https://davidchristiansen.dk/tutorials/nbe/ | ||
| 35 | Mon, Apr 3 12:00 | Dependent Types | ATAPL Chapter 2.6 and Section 6 and 7 of https://davidchristiansen.dk/tutorials/nbe/ | ||
| 36 | Wed, Apr 5 12:00 | Final project presentations | |||
| 37 | Mon, Apr 10 12:00 | Eastern Monday; no class! | |||
| 38 | Wed, Apr 12 12:00 | Final project presentations | |||