Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.


Introduction to programming with dependent types in Scala

via Stepik


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

Taught by

Dmytro Mitin


Start your review of Introduction to programming with dependent types in Scala

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.