# CSCI-B619: Modern Dependent Types

## Spring 2024

This is a graduate seminar on **the modern design of full-spectrum
dependent type theories**, such as the core calculi of proof
assistants like Agda, Coq, and Lean. The goal of this course is to prepare
students to engage with current research on dependent type theory and to
understand the motivations behind recent extensions of these systems. Topics
include extensional, intensional, homotopy, and cubical type theory.

By the end of the course, students will understand:

- What is (full-spectrum dependent) type theory?
- What makes a good type theory, and why are there so many?
- Why is equality so central to type theory, and what is the state of the art?