CS 410/510 - Dependent Types - Spring 2019

image

Dependent types, where types can contain ordinary programs as well as other types, allow us to enforce stronger invariants with our types and, at the same time, to be more flexible. Dependent types are also expressive enough to be used as a logic for mathematics, where a type is a statement and programs with that type count as evidence for the statement. With dependent types, tools from programming can be used to do math, and tools from math can be used for programming.

During the Spring quarter of 2019, I will be teaching a course on thinking in and implementing dependent types at Portland State University.

The primary textbook for this course is The Little Typer. It will be supplemented with additional hand-outs and course notes.

The course meets Mondays and Wednesdays, 4:30–6:30 PM.

Course Goals

Half of the course will be focused on understanding dependent types, through reading, discussion, and exercises. The other half will focus on techniques for implementing a dependent type checker.

After the course, students should be able to:

  • understand and explain the fundamental concepts of dependent type theory, including the concepts of judgment, proposition, proof, introduction and elimination rules, and the different notions of equality;

  • write recursive functions using fold operators;

  • write proofs by induction in type theory;

  • explain the correspondence between (intuitionistic) proofs and (total) programs;

  • show that the constructors of an inductive type are disjoint and injective;

  • prove that equality on some inductive types is decidable;

  • and implement typed lambda calculi in Haskell, in particular:

    • interpreters for untyped lambda calculi,

    • normalizers for typed and untyped lambda calculi,

    • type checkers, using bidirectional type checking.

Prerequisites

CS 320, Principles of Programming Languages, is the formal prerequisite for CS 410. The homework will require familiarity with Haskell, including recursion, do-notation and monadic programming, but it will not make use of any advanced Haskell features. If you can do these things but have not taken CS 320 at PSU, please get in touch.

Non-PSU Students

There has been a significant interest in this course from members of the community in Portland. If you’d like to take the course, but are not currently enrolled at PSU, here’s how to do it:

  • Enroll as a non-degree student. This can be done as soon as you’d like.

  • Determine whether you’d like a grade and transcript. If not, enroll as an auditor. Tuition charges are the same for auditing students.

  • Once the deadline for degree-seeking student enrollment has passed, enroll in the course.

Non-degree-seeking students may enroll in either CS 410 or CS 510. CS 410 costs less than CS 510. Auditing students will receive the same feedback on assignments as students taking the course for a grade.

Questions?

If you’d like to find out more about the course, please don’t hesitate to get ahold of me.