Course Description

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.

Course Materials

This could will use material from the book The Little Typer and the online Programming Languages Foundations in Agda. You can pick up a copy of The Little Typer from the book store or the library. If you cannot find a copy, I may be able to loan you a copy or provide print out of the relevant chapters. You will need to install racket, DrRacket (which should install by default with the standard racket installation), and the Pie language, which can be installed with raco pkg install pie. You will also need to install Agda and a suitable editor; I recommend Emacs. The PLFA Getting Started page contains instructions:


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.


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

Course Schedule

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).

Last updated: Mon, Nov 20 18:33
# 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. The Little Typer, Chapters 1 and 2
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. The Little Typer, Chapter 3.
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. The Little Typer, Chapters 4 and 5;
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.
14 Thu, Oct 12 SURPRISE CLASS; Make-up Monday. Intro. Total Functions and Dependent Types; dependent elimination The Little Typer Chapter 6
15 Sun, Oct 15 11:59 Assignment 3 due. Submit on Gradescope
16 Mon, Oct 16 More dependent elimination; the equality type The Little Typer, Chapter 7 and 8
17 Wed, Oct 18 Typed normalization by evaluation
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;;; Section "Propositional Equality", Page 59:;
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.