Dependent type systems are advanced type systems that enable program verification and mechanized formal mathematics through well-typed programming. In this course, we'll learn the basics of what dependent types are, how to use them for verify simple programs and mathematical results, and how they're implemented.
This could will use material from the book
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. It will be helpful to be familiar with basic typed functional programming. 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. However, we will cover the basic techniques and theory necessary to implement a language.
This course will involve twice weekly lectures and discussions with in-class programming activities. There will be weekly programming assignments and assigned readings. Students should come to class prepared to discuss readings, ask questions, and work on in-class programming activities. Be sure to bring a laptop with the above software installed and setup correctly.
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
| Participation | 25% |
| Assignments | 75% |
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/winterterm12023/cpsc539b.
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 | Wed, Sep 6 | NO CLASS; ICFP | |||
| 1 | Mon, Sep 11 | Course intro; setup and test activities; PL and Type Theory Basics | |||
| 2 | Wed, Sep 13 | Formalizing judgments; Natural numbers, and Pairs in Pie. | |||
| 3 | Sun, Sep 17 11:59 | Assignment 1 due. | Submit on Gradescope | ||
| 4 | Mon, Sep 18 | Formalizing `same as`; Eliminators for Naturals, in Agda. | |||
| 5 | Wed, Sep 20 | Interpreters, alpha equivalence. | |||
| 6 | Sun, Sep 24 11:59 | Assignment 2 due. | Submit on Gradescope | ||
| 7 | Mon, Sep 25 | NO CLASS; Shonan. | |||
| 8 | Wed, Sep 27 | NO CLASS; Shonan. | |||
| 9 | Mon, Oct 2 | NO CLASS; National Day of Truth and Reconciliation | |||
| 10 | Wed, Oct 4 | Closures; First-class functions and Lists. | |||
| 11 | Sun, Oct 8 23:59 | Assignment 2b due. | Submit on Gradescope | ||
| 12 | Mon, Oct 9 | NO CLASS; Thanksgiving | |||
| 13 | Wed, Oct 11 | Bidirectional typing. | https://davidchristiansen.dk/tutorials/bidirectional.pdf https://davidchristiansen.dk/tutorials/nbe/#%28part._.Bidirectional_.Type_.Checking%29 https://davidchristiansen.dk/tutorials/implementing-types-hs.pdf |
||
| 14 | Thu, Oct 12 | SURPRISE CLASS; Make-up Monday. Intro. Total Functions and Dependent Types; dependent elimination | |||
| 15 | Sun, Oct 15 11:59 | Assignment 3 due. | https://davidchristiansen.dk/tutorials/nbe/#%28part._untyped-norm%29 | Submit on Gradescope | |
| 16 | Mon, Oct 16 | More dependent elimination; the equality type | |||
| 17 | Wed, Oct 18 | Typed normalization by evaluation | https://davidchristiansen.dk/tutorials/nbe/#%28part._typed-nbe%29 | ||
| 18 | Sun, Oct 22 11:59 | Assignment 4 due | Submit on Gradescope | ||
| 19 | Mon, Oct 23 | Induction on naturals and equality (cong) | Chapter 8 and 9 | ||
| 20 | Wed, Oct 25 | Induction on naturals and equality (replace, symm) | |||
| 21 | Fri, Oct 27 | Last day for drop with W. | |||
| 22 | Sun, Oct 29 11:59 | Assignment 5 due | |||
| 23 | Mon, Oct 30 | Induction on lists | Chapter 10 | ||
| 24 | Wed, Nov 1 | Induction on lists | Chapter 11 | ||
| 25 | Sun, Nov 5 11:59 | Assignment 6 due | |||
| 26 | Mon, Nov 6 11:59 | Properties as Types | Chapter 12 | ||
| 27 | Wed, Nov 8 11:59 | The rest of the algebra: Either; Trivial; Absurd | Chapter 13, 14 | ||
| 28 | Sun, Nov 12 11:59 | Assignment 7 due | |||
| 29 | Mon, Nov 13 | NO CLASS; Mid-term break. | |||
| 30 | Wed, Nov 15 | NO CLASS; Mid-term break. | |||
| 31 | Mon, Nov 20 | Consequence, sameness, and equality | Chapter 15 | ||
| 32 | Wed, Nov 22 | Consequence, sameness, and equality | |||
| 33 | Sun, Nov 26 11:59 | Assignment 8 due | |||
| 34 | Mon, Nov 27 11:59 | Decidability | Chapter 16 | ||
| 35 | Wed, Nov 29 11:59 | Equality--Axioms I, K, J; Reflection | Chapter 1.2 of https://www2.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf; https://ncatlab.org/nlab/show/uniqueness+of+identity+proofs; https://ncatlab.org/nlab/show/axiom+K+%28type+theory%29; Section "Propositional Equality", Page 59: http://people.csail.mit.edu/jgross/personal-website/papers/academic-papers-local/Martin-Lof80.pdf; https://ncatlab.org/nlab/show/identity+type | ||
| 36 | Sun, Dec 3 11:59 | Assignment 9 due | |||
| 37 | Mon, Dec 4 11:59 | Topics | |||
| 38 | Wed, Dec 6 11:59 | Topics | |||
| 39 | Thu, Dec 7 | Last day of lecture. | |||