Introduction to programming with dependent types in Scala

This course is an introduction to type theory, homotopy type theory (HoTT), dependent-type programming, type-level programming, and theorem proving using Scala. It covers such topics as dependent types (including path dependent types), type families, sum and product types, functions, dependent Σ- and Π-type, inductive types, identity type, type classes, eliminators (recursion and induction), β-reduction, η-conversion, Curry–Howard isomorphism, programming at type level.

1. Installing software
2. Boolean type
3. ProvingGround DSL
4. Type of natural numbers
5. Combining booleans and natural numbers
6. List type
7. Dependent types
8. Type classes. Simulacrum
9. Product type
10. Co-product type (sum type)
11. Function type
12. Empty and unit types
13. Type family List(A)
14. Dependent pair type (Σ-type)
15. Dependent function type (Π-type)
16. Type of length-indexed vectors
17. Heterogeneous list (HList)
18. Matrices
19. Identity type. Curry–Howard correspondence
20. Eliminators into dependent types (induction)
21. Type-level programming. Shapeless